abstract: Hoare monitors, invented by Brinch Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the High-Assurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, […]

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

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

This was an April Fool’s post published on April 1, 2016. The Imperfect Stitch Compiler is a fictional product. 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, […]

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

abstract: We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that […]

abstract: The Curry-Howard Isomorphism motivates the well known proofs-as-programs interpretation. Under that interpretation, sufficiently different proofs yield different programs. This work is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example, we discovered that the standard type bind (M a -> (a -> M b) -> […]

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.

abstract: Animal movement is driven by responses to both social and non-social factors of the environment. Research across species shows that animals do not make decisions based solely on present information, e.g., at time t, but on an integrated assessment of information over recent time, e.g., t-1, t-2, etc. This raises the conundrum of how […]

abstract: The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In […]