3 ms·

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 wr

by 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.
- munin 11y ago
  > You implement a formal spec for a requirement and/or high-level function that takes plaintext as input and outputs ciphertext. this misses the relationship between the size of the plaintext and the ciphertext... edit: part of the problem is tooling, to deal with stuff like this you need dependent types and those do exist, but not in a way that "the programmer on the street" can use...
  - nickpsecurity 11y ago
    It doesn't and you don't. Size should be specified in both the spec (data properties) and the pre-conditions of the function implementing it.

by munin 11y ago

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.

munin 11y ago
> You implement a formal spec for a requirement and/or high-level function that takes plaintext as input and outputs ciphertext. this misses the relationship between the size of the plaintext and the ciphertext... edit: part of the problem is tooling, to deal with stuff like this you need dependent types and those do exist, but not in a way that "the programmer on the street" can use...
- nickpsecurity 11y ago
  It doesn't and you don't. Size should be specified in both the spec (data properties) and the pre-conditions of the function implementing it.