Rust: from POPL to practice

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

Read More

Galois: 2016 highlights

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

Read More

Tech talk: Verified Secure Computing using Trusted Hardware

abstract: Security-critical applications constantly face threats from exploits in lower computing layers such as the OS and Hypervisor, or even attacks from malicious administrators. To protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX. Intel SGX instructions enable user mode applications to package trusted code […]

Read More

Tech talk: Internet of Things: From Small- to Large-Scale Orchestration

abstract: The domain of Internet of Things (IoT) is rapidly expanding beyond research and becoming a major industrial market with such stakeholders as major manufacturers of chips and connected objects, and fast-growing operators of low-power wide-area networks. Importantly, this emerging domain is driven by applications that leverage the infrastructure to provide users with innovative, high-value […]

Read More

CyberChaff at Reed College

Formaltech, a Galois subsidiary, and Reed are excited to celebrate CyberChaff’s first month of service at Reed. Formaltech’s CyberChaff allows you to deploy low-cost, secure decoy hosts on a network. The hosts alert administrators when an attacker is detected while also slowing down key steps in the attacker’s workflow. In March, Galois and Formaltech engineers […]

Read More

Tech talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency.

abstract: Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where […]

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

Tech talk: Adversarial Machine Learning, Privacy, and Cybersecurity in the Age of Data Science

abstract: Due to the exponential growth of our ability to collect, centralize, and share data in recent years we have been able tackle problems previously assumed to be insurmountable. Ubiquitous sensors, fast and efficient machine learning, and affordable commercial-off-the-shelf technologies have not only deepened our understanding of our world, but also democratized these capabilities. As […]

Read More