Asymmetric Network Defense: Guest blog post by David Archer

Defending networks is becoming increasingly harder, as adversaries are advancing far quicker than our defense techniques. In this guest blog post on Tripwire’s The State of Security blog, David Archer, research lead at Galois, talks about some of the reasons behind this asymmetry, and gives a few ideas on how network defense might catch up […]

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

Tech talk: Evidence-based Trust of Symbolic Execution-based Verification

abstract: Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in […]

Read More

Tech Talk: Viper: Verification Infrastructure for Permission-based Reasoning

abstract: Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from […]

Read More

Tech talk: A Brief History of Verifiable Elections

abstract: Since the ideas were first published in 1981, verifiable election technologies have undergone decades of research successes and deployment failures. This talk will trace the history of these technologies, their evolution, and the practical challenges that they have faced. We’ll then look forward at the potential for near-term successes and the public benefits that […]

Read More

Tech talk: Effective Verification of Low-Level Software with Nested Interrupts

abstract: Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent […]

Read More

Tech talk: An Overview of Emerging Cybersecurity Policy and Law

abstract: Why is cybersecurity such a hard problem? The US government, its citizens, and the organizations that write software are all on the same team, but in many cases, our interests are just not aligned. For instance, there have been endless political and social disagreements about the best way to share cyber threat intelligence without […]

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

Tech talk: The CH2O project: making sense of the C standard

abstract: CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent. There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and […]

Read More