21–30 of 86 posts
Does formal verification protect against buffer overflows? (it's a serious question)
We are investigating ways how to do more formal verification for the implementation itself.
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.
Earlier quoted context omitted.
They verified the protocol, not the actual implementation: 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.
Related: Coq - https://coq.inria.fr/ And CompCert, a formally verified C compiler written in Coq: https://compcert.org/ (even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
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.
I'm too stupid to understand the crypto technicalities. Is this really a good solution? Or embrace, extend, extinguish targeted on Wireguard? The paper abstract mentions a "cookie"-like concept, and from websec I know that cookies are not always the optimal solution and historically cookie implementations had a lot of attack surface. EDIT: Seems to come from German Max-Planck Institute which is funded by German gover…
I'm too stupid to understand the crypto technicalities. Is this really a good solution? Or embrace, extend, extinguish targeted on Wireguard? The paper abstract mentions a "cookie"-like concept, and from websec I know that cookies are not always the optimal solution and historically cookie implementations had a lot of attack surface. EDIT: Seems to come from German Max-Planck Institute which is funded by German gover…
The cookie thing is a defense against WireGuard CVE-2021-46873; the attack is in my view not bad enough to get rid of the WireGuard protocol. WG is still the standard for pre-quantum VPN implementations. Rosenpass also needs to use post-quantum crypto-primitives that need a lot of cpu and memory resources.
Rosenpass and WireGuard work together; Rosenpass runs in userspace and gives keys to WireGuard so we do not plan to replace it any time.
It would be possible to apply the biscuit mechanism to classical WireGuard; unfortunately that would cause a protocol incompatibility. I am not sure if they are going to take that path.
Earlier quoted context omitted.
The article refers to a "cookie" as a "biscuit" "Lacking a reliable way to detect retransmission, we remove the replay protection mechanism and store the responder state in an encrypted cookie called “the biscuit” instead. Since the responder does not store any session-dependent state until the initiator is interactively authenticated, there is no state to disrupt in an attack." Both WG and PQWG are vulnerable to sta…
AFAIK a NTP client doesn't accept a value which highly differentiates from the current time. At least, not without user interaction. Does that render this attack less likely?
It does yes. But it is a mitigation, not a real fix.
An attacker could still just speed up time. Although not being able to produce a KillPacket for the year three thousand is a good thing :)
Earlier quoted context omitted.
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.
What is a bug in the spec? Or in a part that was not formally verified?
Essentially the answer depends on who you ask. For my part I would say both.
Why not just use PresharedKey in Wireguard?
We are :) Rosenpass is a fancy way of generating a PSK for WireGuard.
Does formal verification protect against buffer overflows? (it's a serious question)
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.
I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...