5 ms·

Ironsides DNS Server in Ada Spark

46 points by based2 7y ago

capableweb 7y ago
> We describe the development of IRONSIDES, an implementation of DNS that is provably invulnerable to remote code execution exploits and single-packet denial of service attacks Sounds like famous last words. How can something be provably invulnerable to RCE? Wouldn't you just be able to prove that it's invulnerable to known RCE's? From https://ironsides.martincarlisle.com/globecom_2012.pdf https://ironsides.martincarlisle.com/globecom_2012.pdf
- fulafel 7y ago
  Something could be provably invulnerable to RCE the same way other properties of programs are formally proved in computer science. The general class of techniques for software is called "formal methods". A program could also be implemented in a safe language where the defined semantics rule out RCE. Of course this would then depend on how much trust and/or verification is put into the language implementation and specification corectness.
  - tgflynn 7y ago
    > A program could also be implemented in a safe language where the defined semantics rule out RCE. It doesn't seem like such a language would be very useful, unless you mean a language developed specifically for a particular application. A language can be made safe against invalid memory accesses and undefined behavior but if it prevents RCE then it must also prevent implementing remote procedure calls, meaning it's not general purpose.
    - noselasd 7y ago
      Maybe you have a very broad definition of RCE, one that does not match up with RCE as used by security professionals ?
      - tgflynn 7y ago
        I've seen a couple of different definitions, but the most restrictive appears to be that RCE means the ability to execute arbitrary code on a remote host (https://en.wikipedia.org/wiki/Arbitrary_code_execution https://en.wikipedia.org/wiki/Arbitrary_code_execution). Note that the definition returned at the top of a Google search for RCE is considerably more general than this. There are many pieces of software that allow a remote user to execute arbitrary code remotely. Some examples are ssh and the Jupiter notebook running a Python or Julia kernel. Of course these types of software usually include an authentication/authorization mechanism limiting access to authorized users. Any bug in the implementation of this mechanism could potentially allow the unauthorized remote execution of arbitrary code. No "safe" language alone can prove the absence of all such bugs. At a minimum doing so would require a complete specification of who is authorized to execute what code and how they are to prove their identity to the software along with a formal proof that the implementation completely implements the spec.
        deleted 7y ago
        [deleted]
    - tgflynn 7y ago
      It appears some people haven't understood my comment so I will attempt to explain it more fully. First let me be clear that this comment only relates to the parent's statement "A program could also be implemented in a safe language where the defined semantics rule out RCE." It is this claim I take issue with, not anything about the original post, which I haven't looked at in detail. Spark allows contracts and pre- and post- conditions to be defined on procedures which together may amount to encoding a spec for the application into the source code. It may then be possible to prove the implementation correct relative to this spec. But that's very different from saying that the defined semantics of the language alone (ie. without the spec which must be provided to the verifier one way or another) prevents RCE. Now to substantiate my claim that the semantics of a general purpose language cannot alone "rule out RCE". 1) A general purpose language may be used to implement a program which provides an RPC (remote procedure call) mechanism, whether open to all or restricted to a set of authorized users. 2) A program written in a general purpose language may implement an interpreter for its own, or some other language, such as Scheme. 3) In the absence of a formal spec nothing prevents the programmer from implementing an RPC call which takes a string received from the network, with no authorization/authentication checks, and runs that string through the program's scheme interpreter. This constitutes RCE by any definition I'm aware of.
    - fulafel 7y ago
      Yep, of course RCE would have to be precisely defined in the case of this approach. You could have a turing-incomplete language that prevents interpreting, or you could have a more general language that just prevents uncontrolled RCE due to memory safety compromise. Or some formal proof of not interpreting received symbols in a way that affects control flow in a complex way..
- albntomat0 7y ago
  The key is that it’s proven within the formal method system used. For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover
  - MaxBarraclough 7y ago
    > For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. Also, a bug in the compiler could introduce such a bug. To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. > There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover Typically we'd expect the only vulnerabilities in such an implementation would be side-channel attacks, such as timing attacks. Do you have any more details on this? I couldn't find anything with a quick google.
    - albntomat0 7y ago
      Top of the second page: https://link.springer.com/article/10.1007/s00165-012-0269-9 https://link.springer.com/article/10.1007/s00165-012-0269-9 My understanding is that both Needham–Schroeder and SSL had formal verification prior to the breaks, but the breaks relied on properties outside of what was proven (which was thought to be complete at the time).
      - MaxBarraclough 7y ago
        Great, thanks. I found a freely available pre-print at http://alfredo.pironti.eu/research/sites/default/files/cf11.pdf http://alfredo.pironti.eu/research/sites/default/files/cf11.... The relevant content is mostly on page 2. They seem to be saying that when it comes to crypto, both the requirements work and the implementation work are both challenging and error-prone, even for expert practitioners. I don't think they're exactly saying anything against formal methods, though: > It is significant, for example, that the above mentioned flaw affecting the Needham-Schroeder public-key protocol could be found by applying formal methods Later, under Motivation, regarding what are essentially integration bugs: > in OpenSSL an error condition returned by a cryptographic function was incorrectly interpreted by the function caller, making the application accept corrupted data; such a fault cannot be found if a formal model that has no relation with the implementation code is analyzed Not exactly a demonstration of a weakness of formal methods. Instead, an instance of a bug (a normal one, not a side-channel vulnerability) occurring in a system which was only partially formally verified. > a large gap still exists between these models and a real-world protocol implementation and its execution. A problem with real-world implementation, not with formal methods. I wonder what they would have made of 'SPARKSkein', released around the time that paper was published. [0] I suppose it wouldn't have been anything all that new - integration bugs could still occur. [0] https://www.adacore.com/papers/sparkskein https://www.adacore.com/papers/sparkskein
- bjoli 7y ago
  You can prove all sorts of properties about a program. Sometimes the compiler produces bad code, but that is really not the fault of the formal verification, but a compiler bug. Try writing some moderately complex progra. in C, then a formally verified version in SPARK and fuzz them. That is usually quite confidence-inspiring :)
mcejp 7y ago
If you prefer to read code on GitHub: https://github.com/mcejp/IRONSIDES https://github.com/mcejp/IRONSIDES

46 points by based2 7y ago

> We describe the development of IRONSIDES, an implementation of DNS that is provably invulnerable to remote code execution exploits and single-packet denial of service attacks Sounds like famous last words. How can something be provably invulnerable to RCE? Wouldn't you just be able to prove that it's invulnerable to known RCE's? From https://ironsides.martincarlisle.com/globecom_2012.pdf https://ironsides.martincarlisle.com/globecom_2012.pdf

fulafel 7y ago
Something could be provably invulnerable to RCE the same way other properties of programs are formally proved in computer science. The general class of techniques for software is called "formal methods". A program could also be implemented in a safe language where the defined semantics rule out RCE. Of course this would then depend on how much trust and/or verification is put into the language implementation and specification corectness.
- tgflynn 7y ago
  > A program could also be implemented in a safe language where the defined semantics rule out RCE. It doesn't seem like such a language would be very useful, unless you mean a language developed specifically for a particular application. A language can be made safe against invalid memory accesses and undefined behavior but if it prevents RCE then it must also prevent implementing remote procedure calls, meaning it's not general purpose.
  - noselasd 7y ago
    Maybe you have a very broad definition of RCE, one that does not match up with RCE as used by security professionals ?
    - tgflynn 7y ago
      I've seen a couple of different definitions, but the most restrictive appears to be that RCE means the ability to execute arbitrary code on a remote host (https://en.wikipedia.org/wiki/Arbitrary_code_execution https://en.wikipedia.org/wiki/Arbitrary_code_execution). Note that the definition returned at the top of a Google search for RCE is considerably more general than this. There are many pieces of software that allow a remote user to execute arbitrary code remotely. Some examples are ssh and the Jupiter notebook running a Python or Julia kernel. Of course these types of software usually include an authentication/authorization mechanism limiting access to authorized users. Any bug in the implementation of this mechanism could potentially allow the unauthorized remote execution of arbitrary code. No "safe" language alone can prove the absence of all such bugs. At a minimum doing so would require a complete specification of who is authorized to execute what code and how they are to prove their identity to the software along with a formal proof that the implementation completely implements the spec.
      - deleted 7y ago
        [deleted]
  - tgflynn 7y ago
    It appears some people haven't understood my comment so I will attempt to explain it more fully. First let me be clear that this comment only relates to the parent's statement "A program could also be implemented in a safe language where the defined semantics rule out RCE." It is this claim I take issue with, not anything about the original post, which I haven't looked at in detail. Spark allows contracts and pre- and post- conditions to be defined on procedures which together may amount to encoding a spec for the application into the source code. It may then be possible to prove the implementation correct relative to this spec. But that's very different from saying that the defined semantics of the language alone (ie. without the spec which must be provided to the verifier one way or another) prevents RCE. Now to substantiate my claim that the semantics of a general purpose language cannot alone "rule out RCE". 1) A general purpose language may be used to implement a program which provides an RPC (remote procedure call) mechanism, whether open to all or restricted to a set of authorized users. 2) A program written in a general purpose language may implement an interpreter for its own, or some other language, such as Scheme. 3) In the absence of a formal spec nothing prevents the programmer from implementing an RPC call which takes a string received from the network, with no authorization/authentication checks, and runs that string through the program's scheme interpreter. This constitutes RCE by any definition I'm aware of.
  - fulafel 7y ago
    Yep, of course RCE would have to be precisely defined in the case of this approach. You could have a turing-incomplete language that prevents interpreting, or you could have a more general language that just prevents uncontrolled RCE due to memory safety compromise. Or some formal proof of not interpreting received symbols in a way that affects control flow in a complex way..
albntomat0 7y ago
The key is that it’s proven within the formal method system used. For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover
- MaxBarraclough 7y ago
  > For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. Also, a bug in the compiler could introduce such a bug. To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. > There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover Typically we'd expect the only vulnerabilities in such an implementation would be side-channel attacks, such as timing attacks. Do you have any more details on this? I couldn't find anything with a quick google.
  - albntomat0 7y ago
    Top of the second page: https://link.springer.com/article/10.1007/s00165-012-0269-9 https://link.springer.com/article/10.1007/s00165-012-0269-9 My understanding is that both Needham–Schroeder and SSL had formal verification prior to the breaks, but the breaks relied on properties outside of what was proven (which was thought to be complete at the time).
    - MaxBarraclough 7y ago
      Great, thanks. I found a freely available pre-print at http://alfredo.pironti.eu/research/sites/default/files/cf11.pdf http://alfredo.pironti.eu/research/sites/default/files/cf11.... The relevant content is mostly on page 2. They seem to be saying that when it comes to crypto, both the requirements work and the implementation work are both challenging and error-prone, even for expert practitioners. I don't think they're exactly saying anything against formal methods, though: > It is significant, for example, that the above mentioned flaw affecting the Needham-Schroeder public-key protocol could be found by applying formal methods Later, under Motivation, regarding what are essentially integration bugs: > in OpenSSL an error condition returned by a cryptographic function was incorrectly interpreted by the function caller, making the application accept corrupted data; such a fault cannot be found if a formal model that has no relation with the implementation code is analyzed Not exactly a demonstration of a weakness of formal methods. Instead, an instance of a bug (a normal one, not a side-channel vulnerability) occurring in a system which was only partially formally verified. > a large gap still exists between these models and a real-world protocol implementation and its execution. A problem with real-world implementation, not with formal methods. I wonder what they would have made of 'SPARKSkein', released around the time that paper was published. [0] I suppose it wouldn't have been anything all that new - integration bugs could still occur. [0] https://www.adacore.com/papers/sparkskein https://www.adacore.com/papers/sparkskein
bjoli 7y ago
You can prove all sorts of properties about a program. Sometimes the compiler produces bad code, but that is really not the fault of the formal verification, but a compiler bug. Try writing some moderately complex progra. in C, then a formally verified version in SPARK and fuzz them. That is usually quite confidence-inspiring :)

mcejp 7y ago

If you prefer to read code on GitHub: https://github.com/mcejp/IRONSIDES https://github.com/mcejp/IRONSIDES