5 ms·

Does formal verification protect against buffer overflows? (it's a serious question)

by Tepix 4y ago

l-lousy 4y ago
From the read me: As with any application a small risk of critical security issues (such as buffer overflows, remote code execution) exists; the Rosenpass application is written in the Rust programming language which is much less prone to such issues. I think their formal analysis is only security/crypto related, at least for the time being.
- wucke13 4y ago
  [dead]
jraph 4y ago
(my answer is general and not specific to this submission) The question is too broad to be answered, there are many different formal verification techniques (including static formal verification techniques, and also dynamic formal verification techniques which happen at runtime), and you could be formally verifying only specific properties of the system. Now, if your formal verification technique forces you to check that each index you use is within bounds (for instance, by forcing you to write loop invariants for each loop, but that's not sufficient because you can index buffers outside a loop or with something unrelated to the loop invariant), then yes, you have proved that you will not overflow buffers. But those pesky implementations are always imperfect and never totally proved correct, what's more they run on pesky hardware which could have flaws and which is usually not itself perfectly verified, so… And then you have model checking, which is also a formal verification technique. You can prove that you won't overflow buffers… in the model (which is a spec). That proves that your spec is sound and that you can implement it without flaws, but it does not actually check that your implementation is correct, of course. Unless your model checking tool can also build the implementation and this feature is proved correct. edit: it seems my model checking paragraph is more relevant than I expected, this submission is actually about model checking if it checks the protocol (and not the implementation).
ekiwi 4y ago
They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis https://github.com/rosenpass/rosenpass#security-analysis This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.
- jraph 4y ago
  Related: Coq - https://coq.inria.fr/ https://coq.inria.fr/ And CompCert, a formally verified C compiler written in Coq: https://compcert.org/ https://compcert.org/ (even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
  - sevenoftwelve 4y ago
    Author of Rosenpass here; Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq. For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif. For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.
- touisteur 4y ago
  Although it would be a great exercise in hybrid SPARK+Coq proof. If (that's a big if) you can specify your algorithm in SPARK then (I think) you can use either the SPARK automated/guided prover, or when it can't discharge the proof, use some predefined lemmas, and barring that go down to the interactive Coq environment (or Isabelle, I've seen it done once) and discharge the verification conditions. Not sure anyone has published such a multi-layer spec and proof effort /with crypto code in the mix/.
hinkley 4y ago
The code signing project I worked on was formally verified. The whole time they were verifying it I found horrible bugs that needed fixing. One even made it past soft launch. So great job boys but this doesn’t help me.
- jraph 4y ago
  What is a bug in the spec? Or in a part that was not formally verified?
  - hinkley 4y ago
    There are a couple of presentations out there about how challenging it is to use XML-Sig correctly. The XML part introduces a whole raft of ambiguities. Chief amongst them is document.getElementByID() and element.getElementByID() can return different answers. Compression file formats have similar ambiguities you need to work out to avoid doppelgängers, and then also avoid overwriting system files via canonical path bugs. Essentially the answer depends on who you ask. For my part I would say both.
ape4 4y ago
I suppose if its implemented in a language that is formally proven to not allow buffer overflows.
sevenoftwelve 4y ago
Author here: No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does We are investigating ways how to do more formal verification for the implementation itself.
- acaloiar 4y ago
  > No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-std.html https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...
  - emperorcezar 4y ago
    One would think that this would be fixed in the last five years?
    - acaloiar 4y ago
      Certainly. What I don't believe is certain is that only one such vulnerability has ever existed and none exist in Rust today. It's not pedantic to differentiate between mitigating a thing and preventing a thing.
      - hhda 4y ago
        You can add `#![forbid(unsafe_code)]` to your codebase to avoid any unsafe Rust, which should prevent buffer overflows. Obviously it may make writing a codebase somewhat harder.
        usefulcat 4y ago
        Will that restriction also be applied transitively to all dependencies?
        4y ago
rurban 4y ago
My verifier (cbmc) does, the ones they used not. Frama-C/Eye would also catch buffer overflows.
thadt 4y ago
Maybe not in general, but there is really interesting work happening in the area of verified protocols generating safe C code (memory safe, overflow safe, timing safe, etc). In particular Project Everest has a set of verified primitives underlying higher level protocols like TLS and more recently all Noise variants (https://eprint.iacr.org/2022/607 https://eprint.iacr.org/2022/607). As WireGuard is based on a Noise construction, it seems reasonable to hope that once formally verified PQ primitives are in place, a fully verified protocol implementation could be generated?
- api 4y ago
  AFAIK Wireguard is just Noise_IK as an IP tunneling protocol. I’ve seen some draft ideas for Noise patterns using Kyber on a slack I am on, but they’d be different since Kyber is a KEM rather than a Diffie-Hellman type construction. Noise is all built around DH. You can use Kyber alongside Noise in a hybrid construction. Just mix it in with the PSK or something.

Does formal verification protect against buffer overflows? (it's a serious question)

by Tepix 4y ago

Does formal verification protect against buffer overflows? (it's a serious question)

From the read me: As with any application a small risk of critical security issues (such as buffer overflows, remote code execution) exists; the Rosenpass application is written in the Rust programming language which is much less prone to such issues. I think their formal analysis is only security/crypto related, at least for the time being.

wucke13 4y ago
[dead]

jraph 4y ago

(my answer is general and not specific to this submission) The question is too broad to be answered, there are many different formal verification techniques (including static formal verification techniques, and also dynamic formal verification techniques which happen at runtime), and you could be formally verifying only specific properties of the system. Now, if your formal verification technique forces you to check that each index you use is within bounds (for instance, by forcing you to write loop invariants for each loop, but that's not sufficient because you can index buffers outside a loop or with something unrelated to the loop invariant), then yes, you have proved that you will not overflow buffers. But those pesky implementations are always imperfect and never totally proved correct, what's more they run on pesky hardware which could have flaws and which is usually not itself perfectly verified, so… And then you have model checking, which is also a formal verification technique. You can prove that you won't overflow buffers… in the model (which is a spec). That proves that your spec is sound and that you can implement it without flaws, but it does not actually check that your implementation is correct, of course. Unless your model checking tool can also build the implementation and this feature is proved correct. edit: it seems my model checking paragraph is more relevant than I expected, this submission is actually about model checking if it checks the protocol (and not the implementation).

ekiwi 4y ago

They verified the protocol, not the actual implementation: https://github.com/rosenpass/rosenpass#security-analysis https://github.com/rosenpass/rosenpass#security-analysis This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.

jraph 4y ago
Related: Coq - https://coq.inria.fr/ https://coq.inria.fr/ And CompCert, a formally verified C compiler written in Coq: https://compcert.org/ https://compcert.org/ (even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
- sevenoftwelve 4y ago
  Author of Rosenpass here; Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq. For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif. For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.
touisteur 4y ago
Although it would be a great exercise in hybrid SPARK+Coq proof. If (that's a big if) you can specify your algorithm in SPARK then (I think) you can use either the SPARK automated/guided prover, or when it can't discharge the proof, use some predefined lemmas, and barring that go down to the interactive Coq environment (or Isabelle, I've seen it done once) and discharge the verification conditions. Not sure anyone has published such a multi-layer spec and proof effort /with crypto code in the mix/.

hinkley 4y ago

The code signing project I worked on was formally verified. The whole time they were verifying it I found horrible bugs that needed fixing. One even made it past soft launch. So great job boys but this doesn’t help me.

jraph 4y ago
What is a bug in the spec? Or in a part that was not formally verified?
- hinkley 4y ago
  There are a couple of presentations out there about how challenging it is to use XML-Sig correctly. The XML part introduces a whole raft of ambiguities. Chief amongst them is document.getElementByID() and element.getElementByID() can return different answers. Compression file formats have similar ambiguities you need to work out to avoid doppelgängers, and then also avoid overwriting system files via canonical path bugs. Essentially the answer depends on who you ask. For my part I would say both.

ape4 4y ago

I suppose if its implemented in a language that is formally proven to not allow buffer overflows.

sevenoftwelve 4y ago

Author here: No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does We are investigating ways how to do more formal verification for the implementation itself.

acaloiar 4y ago
> No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-std.html https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...
- emperorcezar 4y ago
  One would think that this would be fixed in the last five years?
  - acaloiar 4y ago
    Certainly. What I don't believe is certain is that only one such vulnerability has ever existed and none exist in Rust today. It's not pedantic to differentiate between mitigating a thing and preventing a thing.
    - hhda 4y ago
      You can add `#![forbid(unsafe_code)]` to your codebase to avoid any unsafe Rust, which should prevent buffer overflows. Obviously it may make writing a codebase somewhat harder.
      - usefulcat 4y ago
        Will that restriction also be applied transitively to all dependencies?
        4y ago

rurban 4y ago

My verifier (cbmc) does, the ones they used not. Frama-C/Eye would also catch buffer overflows.

thadt 4y ago

Maybe not in general, but there is really interesting work happening in the area of verified protocols generating safe C code (memory safe, overflow safe, timing safe, etc). In particular Project Everest has a set of verified primitives underlying higher level protocols like TLS and more recently all Noise variants (https://eprint.iacr.org/2022/607 https://eprint.iacr.org/2022/607). As WireGuard is based on a Noise construction, it seems reasonable to hope that once formally verified PQ primitives are in place, a fully verified protocol implementation could be generated?

api 4y ago
AFAIK Wireguard is just Noise_IK as an IP tunneling protocol. I’ve seen some draft ideas for Noise patterns using Kyber on a slack I am on, but they’d be different since Kyber is a KEM rather than a Diffie-Hellman type construction. Noise is all built around DH. You can use Kyber alongside Noise in a hybrid construction. Just mix it in with the PSK or something.