3 ms·

> 2. Mathematical spec of those where English ambiguity could effect results. What does a mathematical specification of "secure" look like?

by munin 11y ago

rnovak 11y ago
I'm guessing he's referring to something like TLA+, which is a "mathematical" language for formal specification/verification of software systems.
- munin 11y ago
  Yes, so what does "secure" look like in TLA+...
  - nickpsecurity 11y ago
    Since you asked about TLA+ specifically... http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s... Amazon notes many kinds of problems that lead to reliability and security failures that TLA+ helped knock out. Their engineers are sold on it now and have no intention of dropping it. Certain sentences in that article are nearly identical to those I read in ancient papers using ancient methods. The benefits of precise, easy-to-analyze specifications are apparently timeless. Here's it done in Z via Altran's Correct by Construction methodology: http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf They apply about every lesson learned in high assurance in their work. Defect rate, from this demo to old Mondex CA, is usually around 0.04 per 1,000 lines of code. That's better than the Linux kernel. Rockwell-Collins formalized a separation architecture, HW, microcode, etc then integrated it into a CPU: http://www.ccs.neu.edu/home/pete/acl206/papers/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/papers/hardin.pdf NICTA, who did seL4 verification, use tools to model stuff in the language that causes security errors then use provers to verify they're used correctly. Example tool: https://ssrg.nicta.com.au/projects/TS/autocorres/ https://ssrg.nicta.com.au/projects/TS/autocorres/ Lots of groups using lots of different tools with great results. The difficulty and impact on time-to-market varies. The use of compositional, functions or state-machine models with subsets of safe languages, design-by-contract (or just interface checks), static analysis, design/code review, testing, and compilation with conservative optimization seem to be the winning combo. There's free tools for all of that. It takes about the same time to code as usual while preventing lots of debugging during testing and integration.
weinzierl 11y ago
Something like this: 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! https://media.ccc.de/v/32c3-7195-verified_firewall_ruleset_verification https://media.ccc.de/v/32c3-7195-verified_firewall_ruleset_v...
- munin 11y ago
  does it? so you can say "yes, we do not allow these ports" or whatever... does that mean it is "secure"? this doesn't check iptables, only the rules that you write using iptables (as far as I can tell) the point I am getting at is that in a firewall product, what you are checking is something like "only those users listed from this source may login" which is "easy" but other more complicated things like "this channel must be encrypted". what does "encrypted" mean? Is it just a word that you use in your specification language? if so, does it mean what you think it means? etc etc etc... formally proving stuff about the behavior of a system, or a distributed system, is hard, but formally proving stuff about security, especially as it relates to information flows, side channels, etc is very hard...
  - nickpsecurity 11y ago
    ""yes, we do not allow these ports" or whatever... does that mean it is "secure"?" No, it means you don't allow those ports. That's all it means. Saying precisely what you're doing or what attributes your aiming for are what the formal work is all about. Whether your security policy is enough and your design embodies it are different things altogether. "what does "encrypted" mean? Is it just a word that you use in your specification language? if so, does it mean what you think it means? etc etc etc..." That's actually one of the easiest things you could ever check in formal systems. It's helpful to think of it like programming. Actually, done side-by-side. You implement a formal spec for a requirement and/or high-level function that takes plaintext as input and outputs ciphertext. This typically uses Red/Black separation model. You also produce and vet an implementation for the encryption module. Now, how to know if something was encrypted in the system before going on the wire? Wait for it... wait for it... answer: it went through the encryption module first while it was initialized and in a state saying it's encrypting. Just like that. Labels and checking at interfaces were used for identifying what went with what and making policy enforcement easier. Note: Guttman has a security kernel in cryptlib that does this at the interface level for every function in the system. In CompSci literature, it's called Assured Pipelines if you want to look it up. Easier to support now with Design-by-Contract and advanced typing systems. Past systems were kludgy when they happened at OS level except with capability systems. Anyway, such components and functions are composed with the interactions and compositions analyzed. Each component and composition usually has a small number of execution traces it can perform so one can brute force the analysis if necessary. Finite state machines, both success and fail states, were common in high assurance development because they can be analyzed in full in all sorts of ways. Note: It was Dijkstra that invented the method for this in the THE multiprogramming system. I think PSOS did it for security first. VAX Security Kernel Retrospective has nice sections where they show layering and assurance activities plus effect they had on analysis and defect hunting. Google any of those to understand the method better.
nl 11y ago
See https://sel4.systems https://sel4.systems
- nickpsecurity 11y ago
  One of the best in the field. :) Although I think they just have dev assurance. Not total high assurance. An early one with total was GEMSOS by Schell, one of INFOSEC's founders: http://www.iwia.org/2005/Schell2005.PDF http://www.iwia.org/2005/Schell2005.PDF Smartcard OS by Karger, another founder of INFOSEC: https://www.acsac.org/2012/workshops/law/pdf/Lessons.pdf https://www.acsac.org/2012/workshops/law/pdf/Lessons.pdf A comparable one for dev assurance, but maybe easier to emulate, was CompCert. Testing of it against many other compilers validated formal verification gave best reliability. http://gallium.inria.fr/~xleroy/talks/compcert-lctes08.pdf http://gallium.inria.fr/~xleroy/talks/compcert-lctes08.pdf Ironically, Microsoft compete neck-to-neck with seL4 in terms of verification with their excellent work on VerveOS: https://people.csail.mit.edu/jeanyang/papers/pldi117-yang.pdf https://people.csail.mit.edu/jeanyang/papers/pldi117-yang.pd...
- munin 11y ago
  that's a proof that the system corresponds to a specification though
  - nickpsecurity 11y ago
    That's right: a formal specification, formal security model, and proof the spec implements it. An implementation formally proven to implement that spec will then posses the security property unless done in by stuff not covered by that model. Which is where EAL6/7's other assurance activities come in.

> 2. Mathematical spec of those where English ambiguity could effect results. What does a mathematical specification of "secure" look like?

by munin 11y ago

> 2. Mathematical spec of those where English ambiguity could effect results. What does a mathematical specification of "secure" look like?

rnovak 11y ago

I'm guessing he's referring to something like TLA+, which is a "mathematical" language for formal specification/verification of software systems.

munin 11y ago
Yes, so what does "secure" look like in TLA+...
- nickpsecurity 11y ago
  Since you asked about TLA+ specifically... http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s... Amazon notes many kinds of problems that lead to reliability and security failures that TLA+ helped knock out. Their engineers are sold on it now and have no intention of dropping it. Certain sentences in that article are nearly identical to those I read in ancient papers using ancient methods. The benefits of precise, easy-to-analyze specifications are apparently timeless. Here's it done in Z via Altran's Correct by Construction methodology: http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf They apply about every lesson learned in high assurance in their work. Defect rate, from this demo to old Mondex CA, is usually around 0.04 per 1,000 lines of code. That's better than the Linux kernel. Rockwell-Collins formalized a separation architecture, HW, microcode, etc then integrated it into a CPU: http://www.ccs.neu.edu/home/pete/acl206/papers/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/papers/hardin.pdf NICTA, who did seL4 verification, use tools to model stuff in the language that causes security errors then use provers to verify they're used correctly. Example tool: https://ssrg.nicta.com.au/projects/TS/autocorres/ https://ssrg.nicta.com.au/projects/TS/autocorres/ Lots of groups using lots of different tools with great results. The difficulty and impact on time-to-market varies. The use of compositional, functions or state-machine models with subsets of safe languages, design-by-contract (or just interface checks), static analysis, design/code review, testing, and compilation with conservative optimization seem to be the winning combo. There's free tools for all of that. It takes about the same time to code as usual while preventing lots of debugging during testing and integration.

weinzierl 11y ago

Something like this: 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! https://media.ccc.de/v/32c3-7195-verified_firewall_ruleset_verification https://media.ccc.de/v/32c3-7195-verified_firewall_ruleset_v...

munin 11y ago
does it? so you can say "yes, we do not allow these ports" or whatever... does that mean it is "secure"? this doesn't check iptables, only the rules that you write using iptables (as far as I can tell) the point I am getting at is that in a firewall product, what you are checking is something like "only those users listed from this source may login" which is "easy" but other more complicated things like "this channel must be encrypted". what does "encrypted" mean? Is it just a word that you use in your specification language? if so, does it mean what you think it means? etc etc etc... formally proving stuff about the behavior of a system, or a distributed system, is hard, but formally proving stuff about security, especially as it relates to information flows, side channels, etc is very hard...
- nickpsecurity 11y ago
  ""yes, we do not allow these ports" or whatever... does that mean it is "secure"?" No, it means you don't allow those ports. That's all it means. Saying precisely what you're doing or what attributes your aiming for are what the formal work is all about. Whether your security policy is enough and your design embodies it are different things altogether. "what does "encrypted" mean? Is it just a word that you use in your specification language? if so, does it mean what you think it means? etc etc etc..." That's actually one of the easiest things you could ever check in formal systems. It's helpful to think of it like programming. Actually, done side-by-side. You implement a formal spec for a requirement and/or high-level function that takes plaintext as input and outputs ciphertext. This typically uses Red/Black separation model. You also produce and vet an implementation for the encryption module. Now, how to know if something was encrypted in the system before going on the wire? Wait for it... wait for it... answer: it went through the encryption module first while it was initialized and in a state saying it's encrypting. Just like that. Labels and checking at interfaces were used for identifying what went with what and making policy enforcement easier. Note: Guttman has a security kernel in cryptlib that does this at the interface level for every function in the system. In CompSci literature, it's called Assured Pipelines if you want to look it up. Easier to support now with Design-by-Contract and advanced typing systems. Past systems were kludgy when they happened at OS level except with capability systems. Anyway, such components and functions are composed with the interactions and compositions analyzed. Each component and composition usually has a small number of execution traces it can perform so one can brute force the analysis if necessary. Finite state machines, both success and fail states, were common in high assurance development because they can be analyzed in full in all sorts of ways. Note: It was Dijkstra that invented the method for this in the THE multiprogramming system. I think PSOS did it for security first. VAX Security Kernel Retrospective has nice sections where they show layering and assurance activities plus effect they had on analysis and defect hunting. Google any of those to understand the method better.

nl 11y ago

See https://sel4.systems https://sel4.systems

nickpsecurity 11y ago
One of the best in the field. :) Although I think they just have dev assurance. Not total high assurance. An early one with total was GEMSOS by Schell, one of INFOSEC's founders: http://www.iwia.org/2005/Schell2005.PDF http://www.iwia.org/2005/Schell2005.PDF Smartcard OS by Karger, another founder of INFOSEC: https://www.acsac.org/2012/workshops/law/pdf/Lessons.pdf https://www.acsac.org/2012/workshops/law/pdf/Lessons.pdf A comparable one for dev assurance, but maybe easier to emulate, was CompCert. Testing of it against many other compilers validated formal verification gave best reliability. http://gallium.inria.fr/~xleroy/talks/compcert-lctes08.pdf http://gallium.inria.fr/~xleroy/talks/compcert-lctes08.pdf Ironically, Microsoft compete neck-to-neck with seL4 in terms of verification with their excellent work on VerveOS: https://people.csail.mit.edu/jeanyang/papers/pldi117-yang.pdf https://people.csail.mit.edu/jeanyang/papers/pldi117-yang.pd...
munin 11y ago
that's a proof that the system corresponds to a specification though
- nickpsecurity 11y ago
  That's right: a formal specification, formal security model, and proof the spec implements it. An implementation formally proven to implement that spec will then posses the security property unless done in by stuff not covered by that model. Which is where EAL6/7's other assurance activities come in.