2019 marked another eventful year for Galois, publishing 15 papers, sharing 26 talks, and announcing several large project awards. It seems cliche, but it’s true: our partners and collaborators play a central role in all of our work. We’re very grateful to be part of such a great community. Below, we highlight some of the […]

Abstract: Developing interactive apps against event-driven software frameworks, like Android, is notoriously difficult. To create apps that behave as expected, developers must follow complex and often implicit asynchronous programming protocols. Such protocols intertwine the proper registering of callbacks to receive control from the framework with appropriate application-programming interface (API) calls that can then in turn […]

2018 was a year of growth and impact at Galois. We furthered our work from cryptography to software and hardware assurance through both our R&D efforts and our spin-out companies. Our team grew significantly, and like most everyone in this industry, we continue to hire. We’ve been fortunate to work with many great partners and […]

Abstract: In this talk, I’ll give a high-level overview of Penn’s Vellvm (Verified LLVM) project, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results, in which we verified memory safety transformations and a variant of LLVM’s mem2reg optimization, focusing on the structure of the proof techniques.  Along the way, […]

Abstract: Verification is often the dominant cost in the design of critical systems. In this talk, we advocate the use of refinement to reason about critical systems. The idea is that a system is correct if all of its observable behaviors are allowed by an abstract system that acts as the specification. For example, to […]

2017 brought continued growth in concern about the trustworthiness of computing systems. The breadth of our work at Galois has grown correspondingly. We opened a third office in Dayton, Ohio, grew past 70 employees, and continue to actively hire. We are grateful to our partners and clients that have helped us successfully develop the projects […]

Abstract: In 2015, a language based fundamentally on substructural typing–Rust–hit its 1.0 release, and less than a year later it has been put into production use in a number of tech companies, including some household names. The language has started a trend, with several other mainstream languages, including C++ and Swift, in the early stages […]

2016 saw a remarkable increase in the awareness and impact of our work in provably secure software and high assurance critical systems. As the year comes to a close, we want to pause and reflect on the intellectual contributions that Galwegians have made as result of that work. Overview This year we partnered with Amazon […]

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.

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 […]