To commemorate the public release of the Software Analysis Workbench (SAW), it seemed fitting to blog about some recent work specifying algorithms in Cryptol and proving properties, leveraging SAW along the way. Cryptol, Galois’s domain specific language for describing cryptographic algorithms, has frequently been demonstrated over individual algorithms and toy problems. Our blog is covered […]
Read More
We are pleased to announce a public preview of the Software Analysis Workbench. The Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAW […]
Read More
“Formal verification methods…should be considered the prime choice for verification of complex and mission-critical software ecosystems.” New vulnerabilities in the software infrastructure we all depend on for privacy are discovered frequently. Thus it was not surprising when an INRIA, MSR, and IMDEA team announced discovery of a significant TLS/SSL vulnerability. The surprise in this announcement was […]
Read More
Dr. David Archer, our cryptography research lead, and Prof. Kurt Rolloff of the New Jersey Institute of Technology recently wrote an article for the IEEE Security and Privacy magazine on the topic of computing on sensitive, encrypted data without decrypting it. The new, groundbreaking process of computing on encrypted data has major implications for businesses that would […]
Read More
Following up on our recent post, Block Ciphers, Homomorphically, we have some new results. In our previous post, we reported on two experiments: a single block-at-a-time evaluation of SIMON 64/128 computed with the HElib homomorphic encryption library, and a parallel, 1800 block-at-a-time evaluation of the same cipher. Our results on the latter have not changed: 1800 […]
Read More
by Brent Carmer and David W. Archer, PhD Our team at Galois, Inc. is interested in making secure computation practical. Much of our secure computation work has focused on linear secret sharing (LSS, a form of multi-party computation) and the platform we’ve built on that technology. However, we’ve also done a fair bit of comparison […]
Read More