Symbolic Software
Bring in the experience and knowledge necessary to help you design, or prove secure, state-of-the-art cryptographic systems for new solutions. We've helped design and formally verify some of the world's most widely used cryptographic protocols.
Comprehensive cryptographic software audits.
Symbolic Software brings wide-ranging experience in cryptographic software audits. Whether you're writing an email client with end-to-end encryption, launching the next cryptocurrency wallet or designing the next authentication framework, we've got you covered.
We've helped produce comprehensive software audit reports for projects written in JavaScript, Go, Rust, Swift, Java, .NET and more. We've helped uncover critical vulnerabilities in PGP encryption within Mozilla Thunderbird. We've helped design more secure device pairing protocols for password managers such as RememBear. We've also worked on auditing and securing vital cryptocurrency technologies, such as MetaMask. Symbolic Software has also worked with the Linux Foundation to audit some of the most important COVID-19 contact tracing apps in Europe.
Research software for cryptography engineers.
Symbolic Software has produced research software for applied cryptographers and engineers that have resulted in peer-reviewed scientific publications:
- Verifpal: Verifpal® is new software for verifying the security of cryptographic protocols. Building upon contemporary research in symbolic formal verification, Verifpal's main aim is to appeal more to real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is much easier to write and understand than the languages employed by existing tools. At the same time, Verifpal is able to model protocols under an active attacker with unbounded sessions and fresh values, and supports queries for advanced security properties such as forward secrecy or key compromise impersonation.
- Noise Explorer: Noise Explorer is an online engine for reasoning about Noise Protocol Framework Handshake Patterns. Noise Explorer allows you to design Noise Handshake Patterns, generate formal verification models, explore a compendium of pre-computed formal verification results, and even generate secure software implementations in Go and Rust.
Our clients and partners.
We're proud of our clients, and we especially cherish the partnerships that we've been able to establish along the way. We frequently collaborate with Cure53, one of the world's leading web security firms and continuously bring in insight from renowned contributors in applied cryptography. Here's what our partners have to say about us:
- “We have been working together with Symbolic Software as auditors for cryptographic software. They are reliable, precise, honest, thorough and think outside the box.” — Mario Heiderich. Director, Cure53.
- “Symbolic Software is run by an accomplished researcher, with significant contributions in the area of applied cryptography. He is also a meticulous programmer well-versed in security, and is therefore the right person for projects that require rigorous design and engineering such as privacy-oriented web applications.” — Jean-Philippe Aumasson. Chief Security Officer, Taurus Group.
Symbolic Software has helped verify the cryptographic security of:
