Noise Explorer-VerifPal
Automated proofs and code generation for secure protocols
Noise Explorer is an online engine for reasoning about Noise Protocol Framework (revision 34) Handshake Patterns. Noise Explorer allows you to design Noise Handshake Patterns, and immediately obtain validity checks that verify if your design conforms to the specification. For visually oriented people, it provides a convenient visualisation in your browser. Noise Explorer can also generate Formal Verification Models and Software Implementations. This allows to instantly generate full symbolic models in the applied pi calculus for any Noise Handshake Pattern that you enter. Using ProVerif, these models can be analyzed against passive and active attackers with malicious principals. The model's top-level process and sophisticated queries are specifically generated to be relevant to your Noise Handshake Pattern, including tests for strong vs. weak forward secrecy and resistance to key compromise impersonation Noise Explorer also automatically generates a secure implementation of your chosen Noise Handshake Pattern design, written in Go. In addition the users can explore a Compendium of Formal Verification Results. Since formal verification for complex Noise Handshake Patterns can take time and require fast CPU hardware, Noise Explorer comes with a compendium detailing the full results of all Noise Handshake Patterns described in the original specification. These results are presented with a security model that is even more comprehensive than the original specification, since it includes the participation of a malicious principal.
- The project's own website: https://noiseexplorer.com
Why does this actually matter to end users?
Secure communication over the internet is critical. Humans however are not infallible, and the same holds for the humans that design the protocols that should make our internet traffic safe. Internet engineers and software developers need to handle a lot of complexity, and even a small oversight or a very improbable scenario or combination of factors can mean breaking part or whole of the protection required The secure technologies we depend on to keep internet communications secure are frequently found to suffer from fundamental design vulnerabilities as well as implementation errors. Truth is, while trust is a fundamental human trait, we should not just trust human intuition to get everything right.
This is where computers can come to help us out, to see if we can underpin that trust in a systematic way. Computers have no problem to exhaustively try out all options, even if it takes them millions and millions of tries. When instructed in the right way, that means their endless combinatorial capabilities can be used to simulate even the most unlikely of events. Again and again, if necessary. A lot of awesome computer science brain power has gone into so called formal proofs. Formal proofs use very strict mathematical modelling to take everything that could possibly happen into account, and prove that the software or protocol at hand does what it is assumed to do. However, as you may imagine, this modelling can get pretty complex and as such is an art in itself - restricting the usage to a very limited set of experts. However, once you have the models right you can actually go a lot further than just prove the protocol: from the model you can automatically generate secure software libraries that you can be sure implement the protocols involved exactly right. This is a guarantee that no human programmer can give.
Noise Explorer is the first of a new generation of open source tool that is helping to democratise these proofs, and bring together community knowledge about protocols and proofs at the same time. It conveniently assists those designing secure channels based on the so called Noise Protocol Framework, which is used in some of the largest messaging tools in the market to protect the confidentiality of the messages sent around. The creators of Noise Explorer have precomputed many different options, and so developers can just take the proofs instead of having to model their protocol and spend a lot of time on setup and computation.
Verifpal is the logical next step. It expands the scope of Noise Explorer to make it applicable for many more protocols that need to be secure. Whether you successfully connect to a wireless network, or see the little green padlock next to a website address - we all want to trust the security behind that. VerifPal is creating a unique tool specifically designed to make it easier to make protocols that will not let us users down.
Run by Symbolic Software
This project was funded through the NGI0 PET Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 825310.
