Recap: The Dayton Digital Transformation Summit

Galois has long been an advocate of utilizing formal approaches, such as mathematics, models, data, artificial intelligence and more, to build better systems. Galois had the privilege to continue this advocacy by supporting the Dayton Digital Transformation Summit, which took place from August 2 – 4, 2022, in partnership with the Air Force Digital Transformation […]

Read More

LAGOON: An Analysis Tool for Open Source Communities

At the Mining Software Repositories (MSR2022) conference in May, we presented our LAGOON tool resulting from the DARPA SocialCyber AIE, and led a discussion session on reducing complexity of machine learning. LAGOON provides a comprehensive platform for analyzing and investigating open-source software (OSS) communities for potentially malicious contributors. This is accomplished by ingesting multiple types […]

Read More

Announcing the Release of Crux 0.6

We are pleased to announce the release of Crux 0.6. Crux is a tool for verifying programs containing inline specifications. Crux works with both C/C++ code (via Crux-LLVM) and Rust code (via Crux-MIR). This release brings a variety of improvements, including: Crux-LLVM now has improved support for LLVM debug metadata when the debug-intrinsics option is […]

Read More

Announcing the Release of Cryptol 2.13.0

We are pleased to announce the release of Cryptol 2.13.0. Cryptol is a language for writing and specifying cryptographic algorithms. This release brings a variety of improvements, including: The sortBy function is now implemented using merge sort instead of insertion sort. This improves both asymptotic and observed performance on sorting tasks. “Type mismatch” errors now […]

Read More

An Essential Tool for Cryptography Development

Cryptography continues to rapidly transform our world. It seems like every day there’s a new story about fully homomorphic encryption, blockchains, and how these technologies secure billions and even trillions of dollars in assets.  We’ve talked about cryptographic algorithms and twice about cryptographic assurance. People who work with these concepts every day have been the […]

Read More

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

I’m excited to announce our paper “ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification” has been accepted to PLDI 2022.  Programs often need to reveal information about private or sensitive data. For example, consider an advertiser who wants to send an advertisement to users near a restaurant. To accomplish this, the advertiser could write […]

Read More

Diversity and Accessibility at POPL 2022

I first attended POPL, the ACM SIGPLAN Symposium on Principles of Programming Languages, in Rome, as a first-year grad student in 2013. It was my first real experience in the programming languages (PL) community. My undergraduate advisor presented a paper I had co-authored at a co-located workshop. I attended the programming languages mentoring workshop (PLMW), […]

Read More

Crux in SV-COMP 2022: A Retrospective

This year Galois participated in the annual Competition on Software Verification (SV-COMP) for the first time with our verification tool, Crux. Preparing Crux to be in competition shape has been a project several years in the making, and we are very pleased to have reached this milestone. In this post, we will take a closer […]

Read More

21st Century Cryptography – Asynchronous ASIC

Prior to spinning out of Galois, engineers from Niobium Microsystems completed work on the 21st Century Cryptography DARPA project. This project developed a proof-of-concept ASIC containing high-performance, low-energy, side-channel resistant implementations of AES-256 cryptographic primitives. These implementations were developed in correct-by-construction fashion, by directly translating formal models of the cryptographic constructs into a hardware implementation […]

Read More

2021: Year in Review

2021. Wow. There it went. And far more interesting than most of us anticipated. While weathering the various world storms, we also managed to keep advancing the cause of building trustworthy computing systems. Galois continued pioneering work in formal methods, high-assurance cryptography, machine learning, data science, rigorous digital engineering, and more. From our virtual perch, […]

Read More