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 Web Services to formally verify subcomponents of the s2n SSL/TLS encryption library, making Amazon’s s2n a leading example of verification applied to industrial cryptographic code. We also shared the tools and techniques that enable such verification in multiple venues. SAW, a core component of our formal verification toolset, was released under a 3-clause BSD license, making it widely available for public use.

In 2016, we continued our work on secure and correct cyber-physical systems software. Among multiple contributions, we published a paper outlining tips and techniques for effectively building high-assurance cyber-physical systems based on experience in DARPA’s High Assurance Cyber Military Systems (HACMS) work.

In the field of network defense and cybersecurity, we held multiple talks on our new DHS-funded effort to an build an innovative DDoS defense mechanism that leverages collaboration between peers to stop DDoS attacks early. We also shared our work on the use of unikernels to deploy and secure low cost microservices, and also used them to build CyberChaff, an effective network defense product.

On the heels of last year’s work on elections technology, we announced Free & Fair, an elections technology spin-off focused on enabling verifiable, transparent and secure elections. Free & Fair took an active part in the national conversation on elections integrity and the future of elections technology. Galois also launched Formaltech, a technology transition spin-off specializing in the commercialization of new technologies derived from research and development, like CyberChaff and FUSE.

Tozny, Galois’s secure authentication and encryption spin-off, announced a developer preview of their new secure database, E3DB, based on the NIST-funded Personal Data Storage project announced last year. Tozny’s authentication technology was also used in the Atlanta Streetcar System ticketing app to enable secure, passwordless authentication.

Our work on securing cyber-physical systems, formal verification and network security was covered in national media throughout the year. This year we announced a $10 million award from DARPA’s CFAR program to leverage software diversity techniques in developing breakthrough cyber defenses for existing and future software systems. We also announced a second award of $6.2 million from DARPA’s Brandeis program to measure the privacy, performance and utility of Brandeis systems. We announced three other major awards, and won many more.

Below are additional details and links to our intellectual highlights of 2016.
Happy holidays from all of us at Galois, we wish you the best in the year to come!

High-assurance Cryptography

Galois Ultra Low Power High Assurance Asynchronous Crypto, Lightweight Crypto 2016

Dr. Joe Kiniry held a talk on ultra low power high assurance crypto at the Lightweight Cryptography Workshop organized by the National Institute of Standards and Technology (NIST). In the talk, Dr. Kiniry presented the results from an R&D project focused on synthesizing low power, high assurance hardware crypto implementations from formal specifications.

Formally verifying the HMAC algorithm in Amazon’s s2n TLS library

In collaboration with Amazon Web Services, Galois formally verified subcomponents of the s2n TLS/SSL encryption library by leveraging the Cryptol and SAW toolsets. SAW was also integrated in the build system in order to perform continuous automated verification as s2n development continues. Dr. Joey Dodds published a series of three posts describing the process of verification in detail, as well as the importance of formal verification for cryptographic implementations in today’s cyber environment. At AWS re:invent, Amazon Web Services’ Byron Cook, held a session on automated formal reasoning and AWS systems, which included an overview of the formal verification work conducted on s2n.

Automated Verification of Real-World Cryptographic Implementations, IEEE Security & Privacy

Dr. Aaron Tomb published a paper in IEEE Security & Privacy (Volume: 14, Issue: 6, Nov.-Dec. 2016) detailing approaches and tools like Cryptol and SAW that make it possible to automatically and rigorously verify real-world cryptographic implementations against machine-readable specifications.

Top-to-bottom Verification of Cryptographic Code, MVD 2016

Dr. Aaron Tomb gave the keynote talk on comprehensively verifying cryptographic algorithms at the Midwest Verification Day (MVD) 2016, hosted at Iowa State University. Dr. Tomb described recent advancements that have shown that top-to-bottom verification of cryptographic code is quite practical and walked through a variety of real-world case studies, most involving verification of code that is actively used in production today.

Intro to Cryptol and High-Assurance Crypto Engineering (video), LambdaConf 2015

Adam Foltzer introduced Cryptol at LambdaConf 2015 (video published in 2016). Foltzer implemented and checked a classical cryptosystem in order to teach the basic syntax and semantics of the language, check correctness through the use of QuickCheck and SMT, and demonstrate how the theorem-driven development approach reveals a bug that requires a revision of the cipher.

High-assurance Cryptography, RWC 2016

Dr. Joe Kiniry presented the tools and techniques used at Galois to build and formally verify cryptographic implementations at the Real World Cryptography Conference 2016. Dr. Kiniry walked the audience through the Galois High Assurance Crypto Tool Suite which includes Cryptol and SAW. He also touched on using a subset of tools to automatically synthesize provably correct hardware and software cryptographic implementations.

Maturity and Performance of Programmable Secure Computation, IEEE Security & Privacy.

Dr. David Archer was part of a team that published a review of the state of the art in secure computation in IEEE Security & Privacy, Sep/Oct 2016 Vol 14, No. 5. The paper reviewed the results of U.S. and European secure computation research programs and other published literature to present the state of the art in what can be achieved with today’s secure computing technology. The team also included Dan Bogdanov, Benny Pinkas, and Pille Pullonen.

MPC: Practical Dynamic Composition of Operators in Secure Computation: VoIP and SQL, DiMACS ORAM, June 2016

Dr. David Archer held an invited talk on multi-party computation at the DiMACS ORAM workshop. In the talk, Dr. Archer presents two use cases where the circuit model for secure computation is impractical and gives way to the RAM model: privacy-preserving signal processing and secure database queries.

5Gen: A Framework for Prototyping Applications Using Multilinear Maps and Matrix Branching Programs, ACM CSS 2016.

Dr. Dave Archer, Dr. Daniel Wagner, Dr. Alex Malozemoff, and Adam Foltzer were part of a team that published a study of applications of multilinear maps (mmaps) in cryptography at the 23rd ACM Conference on Computer and Communications Security (ACM CCS). The paper presents a framework to experiment with mmap application to program obfuscation and multi-input functional encryption (MIFE). Also part of the team: Kevin Lewi, Daniel Apon, Brent Carmer, Dan Boneh, Jonathan Katz, and Mariana Raykova.

Attribute-based Key Exchange with General Policies, ACM CCS 2016.

Dr. Alex Malozemoff was part of a team that published a paper presenting an attribute-based key exchange solution at ACM CCS 2016. The approach combines attribute-based encryption (ABE), and attribute-based credentials (ABCs) with garbled circuits to construct an interactive key exchange solution involving a client that holds a certificate (issued by an authority) vouching for that client’s attributes and a server that holds a policy computable on such a set of attributes. Also part of the team: Vladimir Kolesnikov, Hugo Krawczyk, Yehuda Lindell, and Tal Rabin.

What Else is Revealed by Order-Revealing Encryption? ACM CCS 2016

Tom DuBuisson was part of a team that published a paper analyzing order-revealing encryption leakage at ACM CSS 2016. The paper describes multiple ways in which plaintext information can be extracted from ORE ciphertexts by applying known and new attacks to concrete ORE schemes on non-uniform data. Also part of the team: F. Betül Durak and David Cash.

Software correctness and formal verification

Constructing Semantic Models of Programs with The Software Analysis Workbench, VSTTE 2016.

Dr. Aaron Tomb presented a paper detailing the structure of the Software Analysis Workbench, which was presented at 8th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016). The paper, by Dr. Robert Dockins, Adam Foltzer, Dr. Joe Hendrix, Brian Huffman, Dylan McNamee, and Dr. Aaron Tomb, presents experimental results demonstrating the benefits of SAW’s implementation techniques.

Formal Methods at Galois and Free & Fair, DeepSpec 2016.

Dr. Joe Kiniry presented an overview on the use of formal methods at Galois and Free & Fair, Galois’s election technology spin-off, at DeepSpec 2016. Dr. Kiniry walked through the reasons why formal methods are applicable and effective in elections software by using the Free & Fair tabulator as a case study.

A verified information-flow architecture, Journal of Computer Security

Nathan Collins was part of a team that published a paper detailing a verified information-flow architecture in the Journal of Computer Security, vol. 24, no. 6, pp. 689-734, 2016. The paper presents a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE (a clean-slate design for a highly secure computer system), and a machine-checked end-to-end proof of noninterference for this model. Also part of the team were Arthur Azevedo de Amorim, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. Access the complete paper here and the formal proof here.

Insights on Formal Methods in Cybersecurity, IEEE Computer Society

Dr. Joe Kiniry weighed in on the current use and practice of formal methods in cybersecurity for IEEE Computer Society. Dr. Kiniry stated that the part of the FM community that is looking for opportunities to use FM in practice is growing over time in response to the increasing need for FM in industry, particularly in matters relating to critical systems and cybersecurity.

Binary Static Previrtualization, Navy FST 2016

Dr. Joe Hendrix presented APTREE, a project focused on performing whole-program optimization on binaries, at the Navy Forum for SBIR/STTR transition. The goal of the project is to develop tools that take existing compiled binaries, along with platform-specific supporting libraries, and builds reoptimized binaries tailored for a particular platform. The tools strip identify and strip out unused code that may contain security risk, can relocate fixed addresses to make it harder for adversaries to exploit fixed structures, and apply optimization across library boundaries to enable more efficient code and eliminate redundant operations.

High-assurance cyber-physical systems

Hints for High-Assurance Cyber-Physical System Design, IEEE SecDev 2016

Dr. Lee Pike published and presented a paper on high-assurance cyber-physical system design at the IEEE Cybersecurity Development (SecDev), 2016. The paper outlines several “hints” for designing high-assurance cyber-physical system software based on the lessons learned in DARPA’s HACMS program: (1) Constrain the programming languages, (2) Secure the interfaces, (3) Automate the tedium, (4) The Verifier’s Dilemma, and (5) The mythical verification month. Read the full paper here and see the presentation slides here.

Hints for High-Assurance Cyber-Physical System Design, HCCV 2016

Dr. Pike also gave an invited talk presenting “Hints for High-Assurance Cyber-Physical System Design” at the Workshop on High-Consequence Control Verification. See the abstract of the talk here,

Programming Languages for High-Assurance Autonomous Vehicles, MUSE PI meeting, 2016.

Dr. Lee Pike gave an invited talk describing the use of embedded domain-specific languages (EDSLs) for embedded systems in autonomous vehicles at the MUSE PI meeting. The talk focused on using EDSLs to improve programmer productivity and increase software assurance in the context of building an autopilot for unpiloted aircraft called SMACCMPilot, work performed for DARPA under the High-Assurance Cyber Military Systems (HACMS) program. SMACCMPilot was a “green field” design in which most of the architecture and software were designed from scratch. We will discuss both successes and remaining challenges with our approach.

TrackOS: A Security-Aware Real-Time Operating System, RV 2016

Dr. Lee Pike , Pat Hickey, Trevor Elliott, Eric Mertens, and Dr. Aaron Tomb presented a paper at the 16th International Conference on Runtime Verification describing an approach to control-flow integrity protection for real-time systems. The paper details TrackOS, a security-aware real-time operating system that detects malware in real-time embedded systems. TrackOS does this by checking a task’s control stack against a statically-generated call graph, generated by an abstract interpretation-based tool that requires no source code.

Performance bounds for human machine teaming, RSS 2016

Dr. Peter Trautman gave an invited talk on performance bounds for human machine teaming at the Robotics Science and Systems (RSS) Shared Autonomy and Collaborative Robotics Workshop 2016.

Perspectives on Analysis and Design of Human-Centered Robotics workshop, IROS 2016.

Dr. Peter Trautman gave an invited talk about at the Perspectives on Analysis and Design of Human-Centered Robotics workshop, part of 2016 International Conference on Intelligent Robots and Systems (IROS).

Performance Limits of Human-Machine Interface Technology, ShARP

Dr. Peter Trautman gave a keynote talk on shared control at the AAAI Symposium on Shared Autonomy in Research and Practice.

Performance Bounds for Human Machine Teaming and Design, AFRL S5

Dr. Peter Truatman gave a talk on the mathematical theory of human machine teaming at Air Force Research Laboratory’s Safe & Secure Systems and Software Symposium (AFRL S5).

Cybersecurity

Provenance Segmentation, TaPP ‘16.

Dr. David Archer and Erin Chapman were part of a team that published a paper on provenance segmentation at the 8th USENIX Workshop on the Theory and Practice of Provenance (TaPP), which was hosted in conjunction with ProvenanceWeek. The paper describes segmentation (approximating, compressing or summarizing part or all of the provenance graph) as an approach to garner insights from provenance data, with the goal of securing mainstream systems. Also part of the team: Rui Abreu, James Cheney, Hoda Eldardiry, and Adria Gascón.

Combining computational provenance and anomaly detection to reveal cautious, persistent threats, Provenance-based Security and Transparent Computing Workshop

Dr. David Archer presented ongoing work to detect advanced persistent threats as part of DARPA’s Transparent Computing program at the Provenance-based Security and Transparent Computing workshop, Provenance Week. Dr. Archer described the architecture of the system, the approach on each of these technical efforts, and preliminary results to date. For more information on Galois’s Transparent Computing project, visit the ADAPT project page.

Composition Challenges for Automated Software Diversity, LAW 2016.

Dr. Benjamin Davis presented research performed in collaboration with Dr. Stephen Magill and Dr. Simon Winwood at Galois, as well as David Melski, Per Larsen, Michael Franz, and Stijn Volckaert. The work, presented at the Layered Assurance Workshop (LAW) describes issues that must be considered when composing software diversity transformations and is part of Galois’ RADSS project.

3DCoP: DDoS Defense for a Community of Peers (video), DHS S&T R&D Showcase

Jem Berkes presented 3DCoP, an ongoing research project focused on developing an innovative DDoS defense system, at the DHS S&T R&D Showcase and Technical Workshop. 3DCoP enables a community of peers to collaborate for better DDoS defense. Berkes also presented 3DCoP at BSidesPDX 2016. For more information on 3DCoP, watch the video above or visit the project page.

Collaborative DDoS Defense and New IoT Threats, IEEE Winnipeg Section

Jem Berkes presented current research efforts on collaborative DDoS defense and emerging IoT threats at IEEE Winnipeg Section, University of Manitoba. Berkes presented Galois’s 3DCoP project, and explained the new IoT-based botnet threats that have emerged over the past year. For more information on 3DCoP visit the project page.

Critical Applications for Mobile Roots of Trust (video), DHS S&T R&D Showcase

Erin Chapman presented Galois Mobile Roots of Trust project at the DHS S&T R&D Showcase and Technical Workshop. Chapman walked through the results of the project as well as the current state of the mobile roots of trust ecosystem, their benefits, and uses. For more information on the Mobile Roots of Trust project watch the video above, visit the project page, or watch this informational video.

Mobile Roots of Trust: The Next Step in Mobile Security (video)

Galois published a short informational video explaining mobile roots of trust, their applications and the role they play in the mobile ecosystem, as part of the DHS Mobile Roots of Trust project.

Don’t Lose Track of the Actual Problem: Building Trustworthy Mission-critical Systems, The Roles of Hardware & Software, Hardware Security Workshop

Dr. Joe Kiniry and Dr. Dylan McNamee gave a talk at the Hardware Security Workshop, co-organized by Galois, Mentor Graphics, and Intel. This talk focused on the implications on assurance, capabilities, and business for the application of formal methods on secure hardware, and hence high assurance secure systems.

TFER: Collaboration and Automation for Threat Assessment and Mitigation, HCSS 2016

Dr. David Archer presented TFER, a decision analysis system focused on automating cyber threat analysis and assessment at the High Confidence Software and Systems Conference (HCSS). TFER augments human analysts with automated measurements of a system’s security. This helps determine which threats are most dangerous in the current operational context, which assets are at greatest risk, and which mitigations provide the greatest reduction of risk.

Designing an Evidential Assertion Language for Multiple Analysts, BELIEF 2016.

David Burke published a paper describing the design of an evidence-based language in the proceedings of the 4th International Conference on Belief Functions (BELIEF 2016). The expressive language is designed for use by analysts as part of a decision support system for managing cyber threats. The paper describes how the language design provides flexibility to analysts in terms of expressing and combining evidence, while supporting rich interactions between analysts, and then illustrate our approach with examples.

Wigmore: A Constrain-Based Language for Reasoning About Evidence and Uncertainty, HCSS 2016

David Burke presented Wigmore, the evidence-based language detailed in the BELIEF 2016 paper above, at the High-Confidence Software and Systems Conference (HCSS 2016). From the abstract: “In the cybersecurity realm, we are often dealing with great amounts of uncertainty, and it is our experience that in this domain, we are dealing with events that are better characterized by ambiguity, not risk, primarily due to the fact that the adversary is not best modeled as a natural, stochastic process, but rather, as a sentient, learning entity. We are interested in creating software tools to reason about this kind of uncertainty in order to support effective decision-making in the cyber domain.”

Mixing Communications and Paranoia in the New Cyber Defense, Oregon Cyber Security Day

Dr. Adam Wick gave a talk at the Oregon Cyber Security Day describing a variety of new network defense technologies and tactics at Galois and the concrete projects that have been created as a result, including 3DCoP and CyberChaff, highlighting how these techniques can be reified into next-generation cyber solutions.

Diocletian, Constantine, Bedouin Sayings, and Network Defense, StrangeLoop 2016

Dr. Adam Wick gave a talk at StrangeLoop 2016 on the parallels between border defense in the 4th century Roman Empire and modern day network cyberdefense. Dr. Wick argues that when it comes to protecting networks, we are outnumbered, and any technical superiority we may have had is dwindling. He also talks through how we can apply some of the lessons learned: a reactive style to better protect our networks, designing systems to better survive in the new environment, and the fact that trust is not an all-or-nothing property.

Unikernel Microservices: Build, Test, Deploy, Rejoice. StrangeLoop 2016.

Unikernels are a new mechanism to deploy lightweight, scalable, secure microservices that offer big functionality for relatively low cost. Dr. Adam Wick, Adam Foltzer, and Trevor Elliott held a workshop at StrangeLoop 2016 on designing, building, testing, and deploying microservices using unikernels. The team showed a simple microservice design using the HaLVM, and walked through how to build, test, and deploy it into Amazon’s cloud.

Selling Unikernels: The CyberChaff Experience. QCon SF 2016.

Dr. Adam Wick gave a talk about using unikernels to develop network defense software at QCon SF 2016. Dr. Wick walked through the experience of developing of CyberChaff, a novel network defense solution with unikernels built into its core, why unikernels were appropriate, and the pros and cons of using unikernels in a project.

CyberChaff: HaLVM unikernels protecting corporate networks, unikernel.org

Dr. Adam Wick and Amir Chaudhry published an article detailing network defense through decoy hosts and the use of unikernels to implement CyberChaff securely.

Adam Wick on Security, Formal Methods, Types, Unikernels, HaLVM, DRM (video), QCon 2015

In this interview, Dr. Adam Wick talks about cybersecurity in general and some common pitfalls and possible solutions when it comes to securing systems. Dr. Wick also walks through formal methods and proving program correctness as a possible solution to critical vulnerabilities. Unikernels are also discussed, as an approach to give attackers minimal attack surface for critical applications. The interview was recorded in 2015 and published in 2016.

Datanauts 063: Unikernels vs. Containers (Datanauts Podcast)

Just as containers are finding their place alongside virtual machines in the application landscape, unikernels are emerging as a container alternative. Unikernels strip down an application’s execution environment to the barest essentials, increasing efficiency and reducing attack surface. Dr. Adam Wick joins the Datanauts to explain unikernels and how they differ from containers, discuss what kinds of applications they run, and explore issues like networking, security, and orchestration.

Encryption debate: The issue isn’t strong crypto, it’s easy crypto. NextGov.

Isaac Potoczny-Jones published an article on the 2016 encryption debate on NextGov. In the article, Potoczny-Jones argues that, although strong encryption is perceived as a new development that has spurred the debate, it is actually easy to use and ubiquitous encryption behind it, with strong encryption having been available for a long time.

Personal data services promise user privacy, Network Computing

Isaac Potoczny-Jones published an article about Personal Data Services (PDSs) on Network Computing. In the article, Potoczny-Jones outlined the benefits of PDSs in situations where both strong user data privacy and the ability to share with user consent is required.

Data analysis and machine learning

CAFe: Coarray Fortran Extensions for Heterogeneous Computing, HIPS Workshop, IEEE IPDPS 2016

Dr. Matthew Sottile was part of a team that presented a paper on coarray Fortran extensions targeting emerging hybrid accelerator architectures at the 21st International Workshop On High-Level Parallel Programming Models And Supportive Environments (HIPS) at the 30th IEEE IPDPS conference. The paper presented preliminary work examining how Fortran coarray syntax can be extended to provide simpler access to accelerator architectures. Also part of the team: Craig Rasmussen, Soren Rasmussen, Dan Nagle, and William Dumas.

Array Types for a Graph Processing Language. IEEE IPDPS 2016.

Dr. Matthew Sottile and Dr. Mark Tullsen published a paper in the proceedings of 2016 Graph Algorithms Building Blocks Workshop at the 30th IEEE IPDPS conference presenting HAL (Hierarchical Array Language), a typed language for array processing. HAL was designed to efficiently process and operate with graphs, which are frequently represented and manipulated in the form of arrays encoding their adjacency matrices.

Machine Learning, AI, and Cyber Security, at the Oregon Machine Learning Summit 2016

Dr. David Archer gave an invited talk on the intersection of machine learning and cyber security at the Oregon Machine Learning Summit. Dr. Archer argued that modern cyber conflict is an asymmetric battlefield where cyber network defense operators are at a disadvantage. Dr. Archer then presented the case for machine learning technologies such as anomaly detection and behavior classification as a means to level the battlefield by amplifying the attention of those defenders.

Announcements, events, and releases

Galois formally verified subcomponents of Amazon’s s2n SSL/TLS encryption library

In collaboration with Amazon Web Services, Galois leveraged Cryptol and SAW to verify the HMAC algorithm in the s2n encryption library. Read more.

Galois was awarded a $10m DARPA contract to make legacy systems more secure

Galois announced a $10 million award by the Defense Advanced Research Projects Agency (DARPA) Cyber Fault-tolerant Attack Recovery (CFAR) program to make security vulnerabilities lurking in military and commercial legacy, embedded and other mission critical systems code bases unexploitable. The Galois-led team also includes Trail of Bits, Immunant, and University of California, Irvine. For more information, visit the project page.

Galois and Guardtime Federal were awarded a $1.8M DARPA contract to formally verify blockchain-based integrity monitoring system

Galois and Guardtime Federal announced they have jointly been awarded a $1.8 million contract by the Defense Advanced Research Projects Agency (DARPA) to verify the correctness of Guardtime Federal’s Keyless Signature Infrastructure (KSI). The contract will fund a significant effort that aims to advance the state of formal verification tools and all blockchain-based integrity monitoring systems.

Galois was awarded a $6 million DARPA contract to address advanced persistent threats (APTs) in systems and networks

Galois announced $6 million contract award under a Defense Advanced Research Projects Agency (DARPA) program to develop a system to detect Advanced Persistent Threat (APT) cyber attacks in increasingly complex enterprise network and system environments. The project aims to design a system that enhances network visibility to better detect, understand and manage APT attacks in complex network and system environments. The Galois-led team also includes the University of Edinburgh, PARC (a Xerox company), and the Oregon State University,  For more information, visit project page.

Galois was awarded a $1.7 million DHS contract award to combat DDoS attacks

Galois announced a $1.7 million contract by the Department of Homeland Security (DHS) Science and Technology Directorate (S&T) to create technology that is capable of defending against large and sophisticated Distributed Denial of Service (DDoS) attacks. The contract is part of the DHS S&T Cyber Security Division’s larger Distributed Denial of Service Defenses (DDoSD) program. For more information, visit the project page.

Galois was awarded a $6.2 million DARPA contract to ‘crash test’ system privacy

Galois was awarded a $6.2 Million contract by Defense Advanced Research Projects Agency (DARPA) to measure the privacy, performance and utility of systems for its Brandeis program, which is focused on developing tools and techniques for building systems in which private data may be used only for its intended purpose and no other. The Galois-led team also includes which includes the University of Pennsylvania, the University of Maryland College Park, The Hebrew University of Jerusalem and Charles River Analytics. For more information, visit the project page.

Galois launched Free & Fair, an election technology spinoff that enables verifiable, transparent and secure elections

Free & Fair provides elections services and systems meeting the same reliability and security standards as the US federal government demands for national security. For more information, see the original announcement and visit http://freeandfair.us.

Galois launched Formaltech, a technology transition spin-off specializing in commercializing new technologies

Formaltech turns cutting-edge technology research into application, computer, and network security products for cybersecurity OEMs, application developers and enterprises. For more information, visit https://formal.tech.

CyberChaff at Reed College

Formaltech, a Galois subsidiary, and Reed College, announced the deployment of CyberChaff on a core Reed network. CyberChaff an innovative network defense system that uses cyber deception to thwart detect and slow down advanced persistent threats on a network. For more information on CyberChaff, visit the Formaltech CyberChaff page.

Undirector of Engineering

Jef Bell, engineering and project lead at Galois, published a post explaining the unusual nature of the “director of engineering” position at Galois. The post details two attributes of how we organize ourselves at Galois: having no traditional managers, and leadership by council.

Galois co-organized a day long workshop in hardware security with Intel and Mentor Graphics at Intel.

The workshop focused on the challenges of designing, fabricating, verifying, and using secure hardware.  The workshop had over one hundred attendees from industry and academia.

Galois hosted the third annual summer school on probabilistic programming

As part of the ​Probabilistic Programming for Advancing Machine Learning (PPAML) program, Galois hosted the third of four annual summer schools on the topic. The two week program is designed to teach participants the necessary background on probabilistic programming languages being developed as part of PPAML, and give them an opportunity to work directly with the creators of these languages to solve their own problems using these tools.

Galois spin-off Tozny announced developer preview of new secure database, E3DB

E3DB is a NIST-funded tool for programmers who want to build an end-to-end encrypted database with sharing into their projects. For more information, visit the product page.

Tozny announced Atlanta Streetcar ticketing app has Tozny authentication technology built-in.

Atlanta Streetcar System launched a Moovel transit app today that leverages Tozny technology to enable secure, passwordless authentication. See Tozny announcement here.

Galois released BLT, a solver for bounded integer linear programming problems

BLT is a C/C++ library for solving certain integer linear programming (ILP) problems using techniques that come from the theory of lattices. It is complementary to many existing, traditional ILP solvers in that there are problems it solves very well and very quickly which traditional solvers do not.

Galois released the Software Analysis Workbench (SAW), under a 3-clause BSD license.

We announced that SAW, our formal verification platform, will be available under a 3-clause BSD license.

Galois released ec2-unikernel, a tool to upload unikernels to Amazon EC2

The tool is designed to provide a single-step mechanism for uploading your unikernels to run on Amazon EC2.

Galois released halvm-web, a simple web server for the Haskell Lightweight Virtual Machine (HaLVM).

To learn more about HalVM, visit the github page.

Galois released version 2.4.0 of Cryptol, a custom toolset to design and analyze cryptographic algorithms.

To learn more about Cryptol, visit http://cryptol.net

Galois released an updated version of FreeRTOS for Xen on ARM systems.

Highlights of the update included improved compatibility with new versions of Xen and kernel relocation support.

Galois released LandHere, an extension to the Intel x86_64 instruction set architecture

The extension adds two features to help mitigate code-reuse attacks,

Galois held 8 tech talks on a wide range of topics.

Visit the tech talks page for a complete list and our Vimeo page for publicly available recordings.

Press Coverage Highlights

• Galois elections technology spin off, Free & Fair, saw broad coverage and interviews in publications ranging from Techcrunch to Popular Science. For a complete list of elections related coverage, see the Free & Fair news page.

Research coverage

• Computer Scientists Close In on Perfect, Hack-Proof Code, WIRED
• Even the US military is looking at blockchain technology – to secure nuclear weapons, Quartz
• Department of Homeland Security doles out $1.7 million for DDoS protection, The Washington Times.
• For New Cybersecurity Pilot Program, Collaboration Is Key. Government Technology.
• Consortium Partnership project to attack DDoS. Campus Technology
• Cool tech at AWS re:Invent, Network World
• Galois wins $6.2M contract to support DARPA data privacy program, Washington Technology.
• Portland tech firm Galois spins out new company to make elections more secure. Portland Business Journal
• DARPA looks to measure privacy protection, GCN
• DARPA Awards Galois $10 Million Contract To Secure Legacy Cyber Systems. Defense Daily
• Is Your Network Acting Odd? DARPA’s Latest Tool Aims to Sound the Alarm, Defense One
• New security tool addresses Android app collusion threat, BetaNews

Interviews

• Isaac Potoczny-Jones: Minimum Viable App Doesn’t Mean Minimum Security, DevOps.
• Isaac Potoczny-Jones: Mobile security Q&A: Securing the mobile minimum viable app, CSO.
• David Archer Are cyber compliance requirements getting in the way of security? C4ISR
• David Archer: Marine Corps C2 platform unleashes mission critical data. C4ISR
• David Archer: DoD plans to bolster APT security, C4ISR
• Adam Wick: Zero day attacks: How DoD should defend from the unknown. C4ISR

Other contributions

• Dr. Peter Trautman was a panelist at AAAI Symposium on Shared Autonomy in Research and Practice.
• Dr. Peter Trautman was a panelist at AAAI Symposium on Cross-Disciplinary Challenges for Autonomous Systems.
• Dr. Peter Trautman was a member of the program committee at the International Joint Conference on AI (IJCAI 2016)
• Dr. Lee Pike was on the program committee at the Runtime Verification Conference
• Dr. Lee Pike was on the program committee at the International Symposium on Advances in Embedded Systems and Applications (EMBEDDED’16)
• Dr. Lee Pike was on the program committee at NFM’16 (NASA Formal Methods Symposium)
• Dr. Lee Pike was on the program committee at FMCAD’16
• Dr. Lee Pike was a reviewer for Air Force Office of Scientific Research
• Dr. Lee Pike was a NSF Panelist in 2016.
• Dr. Lee Pike was a guest editor Wireless Commuications, Networking, and Positioning with Unmanned Aerial Vehicles, IEEE Communications Magazine.Read the overview and the articles.
• Dr. Stephen Magill was a program committee member for the 2016 IEEE Computer Security Foundations Symposium (CSF)
• Dr. Stephen Magill was a program committee member for the 2016 International Conference on Trust & Trustworthy Computing (TRUST)
• Stephen Magill was a co-chair of the 2016 High-Confidence Software and Systems Conference (HCSS)
• Dr. Stephen Magill was the co-organizer of the 2016 Logic Mentoring Workshop (LMW)
• Dr. Stephen Magill was an NSF Panelist in 2016
• Dr. Joe Kiniry participated in the Elections Verification Network (EVN) Coordinating Committee as part of a multi-year commitment to EVN.
• Dr. Joe Kiniry continued to be active on the Board of Advisors for Verified Voting, which primarily this year focused on the Presidential Election.
• Dr. Joe Kiniry was on the Editorial Board of the Journal of Elections Technology, the premier journal in the area of elections research.
• Dr. Dave Archer was a program committee member at the Workshop on Ubiquitous Sensing and Actuation (UbSA) via the Internet of Things, IEEE World Forum on IoT, December 2016
• Dr. Dave Archer was the co-chair of Provenance-based Security and Transparent Computing, Provenance Week 2016
• Dr. Alex Malozemoff was an external reviewer for PKC 2017, Eurocrypt 2017, and IEEE Security & Privacy 2017.