New BSD-Licensed SAW Release

A new release of the Software Analysis Workbench (SAW) is now available! This release includes a large collection of new features and bug fixes enabling verification of a wider variety of Java and LLVM programs. A list of changes is available here, along with binaries for a variety of platforms. Additionally, this release changes the […]

Read More

Galois Announces ISC: The Imperfect Stitch Compiler

Portland, OR (April 1, 2016) — Galois is known for building perfect software. But is our software too perfect? The imperfect stitch, or Persian flaw, is a deliberate error in an otherwise perfect work of art. The term derives from the proverb, “a Persian rug is perfectly imperfect, and precisely imprecise.” It signifies the inherent […]

Read More

Galois: 2015 highlights

2015 was an active and productive year at Galois. From numerous awards, to new projects and spin-offs, to a vast array of publications and talks, Galwegians contributed to a wide range of fields this year. In this post, we highlight some of the contributions we made in 2015.

Read More

Fuse Analyzer: Handling runtime permissions in Android 6.0

Galois just announced a tool to help Android developers migrate apps to Android 6, while making the best use of the new Runtime Permissions feature. The Galois tool, Fuse Analyzer: Permissions, analyzes binary Andorid APKs to find the locations where you, as a developer, need to handle permissions more carefully in Android 6. The new Runtime Permissions feature brings […]

Read More

ICFP Programming Contest set to take place this weekend

We’re excited to be organizing this year’s ICFP Programming Contest, the annual programming contest of the International Conference on Functional Programming (ICFP).  This year, the contest starts on Friday 7 August 2015 at 12:00 UTC and ends on Monday 10 August 2015 at 12:00 UTC. There will be a lightning division, ending on Saturday 8 […]

Read More

Applying Cryptol and SAW to Minilock Primitives

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

Announcing the Software Analysis Workbench

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

The “FREAK” TLS/SSL flaw, and related thoughts

“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

On the promises of technology for elections: Joe Kiniry speaks at the Voting and Elections Summit

Earlier this month, the Ninth Annual Voting and Elections Summit examined the most critical and persistent issues surrounding U.S. elections and voter participation. Joe Kiniry, Galois’ election systems expert, gave a talk on the promises of technology to increase the transparency and trustworthiness of elections. Dr. Kiniry discussed the trade-offs that election officials face when […]

Read More