|
|
|
32c3 - Verified Firewall Ruleset Verification |
Si vous voulez bloquer ce service sur vos fils RSS
Si vous voulez nous contacter ou nous proposer un fil RSS
Menu > Articles de la revue de presse : - l'ensemble [ tous | francophone] - par mots clé [ tous] - par site [ tous] - le tagwall [ voir] - Top bi-hebdo de la revue de presse [ Voir]
32c3 - Verified Firewall Ruleset Verification Par SecurityTube.NetLe [2016-01-11] à 11:19:35
Présentation : Verified Firewall Ruleset Verification Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle HOL We develop a tool to verify Linux netfilter iptables firewalls rulesets. Then, we verify the verification tool itself. Warning involves math This talk is also an introduction to interactive theorem proving and programming in Isabelle HOL. We strongly suggest that audience members have some familiarity with functional programming. A strong mathematical background is NOT required. TL DR Math is cool again, we now have the tools for executable math . Also iptables We all know that writing large firewall rulesets can be hard. One huge problem. Let's write a tool to statically verify some properties of our rulesets Now we have three huge problems 1 writing flawless firewall rulesets. 2 making sure that our verification tool does the right thing. 3 making sure that the internal firewall model of our tool corresponds to the real world. In this talk, we will solve these problems from front to back. We focus on problems 2 and 3 . Warning this talk involves math First, we need to specify the behavior of the Linux netfilter iptables firewall. In order to be convincing, this model must be small and simple. It should fit on one slide. However, firewalls can be quite complex and the model must cope with this. For example, looking at man iptables-extensions , we see numerous match conditions. But nobody required that our model must be executable code we will specify the model mathematically. For example, this allows to define arbitrary match conditions. Technically speaking, we define the filtering behavior of iptables in terms of bigstep semantics. Mathematical specifications can be very powerful, in particular when we get to the point where the specification is not directly executable . Enough math, let's write some executable code to do something with our ruleset. For example, unfolding the jumps to user-defined chains, checking that some packets will be certainly blocked, or checking that we got the spoofing protection right. Second, based on our firewall model, we can now prove that our algorithms do the right thing. In contrast to testing, a mathematical proof allows assertions for all possible values. For example For all possible packets, rulesets, and firewall-matching-features, our unfolding algorithm does not change the filtering behavior of the firewall. Yes, we can even show that our tool will still be correct, even if the netfilter team pushes a new matching feature. Finally, we now have a verified verification tool. We can use it to verify our firewall ruleset and finally sleep well at night again. We developed an iptables verification library over the last few years in Isabelle HOL. Isabelle can export executable definitions i.e. our algorithms to functional languages such as Haskell, Scala, SML, or OCcaml. Writing the input output functions manually in Haskell, we have a fast and stand-alone tool. This talk is also an introduction to interactive theorem proving and programming in Isabelle HOL. We strongly suggest that audience members have some familiarity with functional programming. A strong mathematical background is not required. For More Information Please Visit - https events.ccc.de category congress 32c3
Les mots clés de la revue de presse pour cet article : firewall
Les videos sur SecuObs pour les mots clés : firewall
Les mots clés pour les articles publiés sur SecuObs : firewall
Les éléments de la revue Twitter pour les mots clé : firewall
Les derniers articles du site "SecurityTube.Net" :
- TROOPERSCON - Crypto code the 9 circles of testing
- TROOPERSCON - Towards a LangSec Aware SDLC
- TROOPERSCON - Deep dive into SAP archive file formats
- TROOPERSCON - Thanks SAP for the vulnerabilities. Exploiting the unexploitable
- TROOPERSCON - An easy way into your multi-million dollar SAP systems An unknown default SAP account
- TROOPERSCON - One Tool To Rule Them All
- TROOPERSCON - Mind The Gap - Exploit Free Whitelisting Evasion Tactics
- TROOPERSCON - The Chimaera Processor
- TROOPERSCON - Lets Play Hide and Seek in the Cloud
- TROOPERSCON - Planes, Trains and Automobiles The Internet of Deadly Things
Menu > Articles de la revue de presse : - l'ensemble [ tous | francophone] - par mots clé [ tous] - par site [ tous] - le tagwall [ voir] - Top bi-hebdo de la revue de presse [ Voir]
Si vous voulez bloquer ce service sur vos fils RSS :
- avec iptables "iptables -A INPUT -s 88.190.17.190 --dport 80 -j DROP"
- avec ipfw et wipfw "ipfw add deny from 88.190.17.190 to any 80"
- Nous contacter par mail
| Mini-Tagwall des articles publiés sur SecuObs : | | | | sécurité, exploit, windows, attaque, outil, microsoft, réseau, audit, metasploit, vulnérabilité, système, virus, internet, usbsploit, données, source, linux, protocol, présentation, scanne, réseaux, scanner, bluetooth, conférence, reverse, shell, meterpreter, vista, rootkit, détection, mobile, security, malicieux, engineering, téléphone, paquet, trames, https, noyau, utilisant, intel, wishmaster, google, sysun, libre |
| Mini-Tagwall de l'annuaire video : | | | | curit, security, biomet, metasploit, biometric, cking, password, windows, botnet, defcon, tutorial, crypt, xploit, exploit, lockpicking, linux, attack, wireshark, vmware, rootkit, conference, network, shmoocon, backtrack, virus, conficker, elcom, etter, elcomsoft, server, meterpreter, openvpn, ettercap, openbs, iphone, shell, openbsd, iptables, securitytube, deepsec, source, office, systm, openssh, radio |
| Mini-Tagwall des articles de la revue de presse : | | | | security, microsoft, windows, hacker, attack, network, vulnerability, google, exploit, malware, internet, remote, iphone, server, inject, patch, apple, twitter, mobile, virus, ebook, facebook, vulnérabilité, crypt, source, linux, password, intel, research, virtual, phish, access, tutorial, trojan, social, privacy, firefox, adobe, overflow, office, cisco, conficker, botnet, pirate, sécurité |
| Mini-Tagwall des Tweets de la revue Twitter : | | | | security, linux, botnet, attack, metasploit, cisco, defcon, phish, exploit, google, inject, server, firewall, network, twitter, vmware, windows, microsoft, compliance, vulnerability, python, engineering, source, kernel, crypt, social, overflow, nessus, crack, hacker, virus, iphone, patch, virtual, javascript, malware, conficker, pentest, research, email, password, adobe, apache, proxy, backtrack |
|
|
|
|
|
