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 contributions we made in 2019.
Overview
2019 was another eventful year for the technical area of secure computation. We announced a $15 million partnership with IARPA to make secure computation, the process of working with data without ever exposing it, accessible to data scientists and other programmers who are not experts in cryptography. We continued to demonstrate and discuss the practical uses of secure computation through numerous talks and publications. We also spoke about using differential privacy to analyze data without revealing information about individuals.
This year, we kicked off a public hardware red-teaming effort at DEF CON to evaluate the security of DARPA SSITH processors, which aim to protect systems against classes of hardware vulnerabilities exploited through software. The red-teaming effort seeks to allow hackers to perform their own security evaluations on mock demonstration systems of the hardware prototypes. Secure processors would address a critical area of concern for DoD and industrial users alike: hardware vulnerability attacks.
In the area of software correctness, we continue to collaborate with Amazon Web Services (AWS) to verify the correctness of security-critical cloud infrastructure. We spoke about model-driven testing approaches used to find and remediate high-priority bugs in key software used to communicate with hardware security modules (HSMs). We also shared a significant number of talks and publications on formal verification, programming language design, type theory, and other programming language concepts.
Additionally, we launched Muse Dev, a spin-off company focused on developing tools that help you find critical bugs early in the development process. Muse Dev is serving a number of early, private beta customers. We have shared a number of talks that illustrate the problems the Muse Dev team is tackling.
Relating to cybersecurity, we announced a $8.6 Million contract awarded as part of DARPA’s CHESS program to build a cyber reasoning tool for vulnerabilities. We have partnered with Harvard University and Trail of Bits and aim to build scalable and more cost-effective tools that identify hard-to-find vulnerabilities.
The team behind our elections security spin-off, Free & Fair, partnered with Microsoft’s Defending Democracy program to develop and release the ElectionGuard SDK. ElectionGuard is a software development kit that enables end-to-end verifiable elections technology. It is open source and available for anyone to use and deploy.
As we tackled that exciting work, the health of the Galois community was a major focus for us in 2019. We strive to improve how we work together. Among other things, this year we reevaluated parental leave, making it 16 weeks for all new parents, and pursued an increased focus on ensuring an inclusive workspace and company activities. On Life at Galois, we share details about how we organize ourselves, which we consider to be a staple of our well-being at Galois. We added some fun ‘color’ relating to our role of Project Lead at Galois and what it entails.
Below you’ll find links to the papers, talks, and other public contributions we made in 2019, as well as other miscellaneous news. We hope you find something interesting.
From all of us at Galois, we wish you a happy 2020.
High Assurance Cryptography
Assuring Real-World Differential Privacy, FMfSS
Dr. José Manuel Calderón Trilla and Dr. Scott Moore gave a talk on differential privacy at the Workshop on Formal Methods for Statistical Software (FMfSS). The talk described motivations behind using differential privacy to analyze data without revealing information about individuals, and gave an overview of approaches to verifying that differential privacy implementations are correct.
RAMPARTS: A Programmer-Friendly System for Building Homomorphic Encryption Applications, WAHC@CCS 2019
Dr. David W. Archer, Dr. José Manuel Calderón Trilla, Jason Dagit, and Dr. Alex J. Malozemoff were part of a team that published a paper on a project that aims to make Homomorphic Encryption, an emerging technology that enables computing on data while data is encrypted, easier to use and implement. Also part of the team: Yuriy Polyakov, Kurt Rohloff, Gerard W. Ryan.
Privacy-Preserved Data Sharing for Evidence-Based Policy Decisions, Bipartisan Policy Center
Dr. David Archer, along with partners at Allegheny County, PA and the Bipartisan Policy Center, published a white paper on privacy-preserving data analysis. The paper outlines a demonstration project that uses multiparty computation to achieve improved data analysis and tangible privacy protections for public policy decision-making. From the paper: “This project used real-world government data to illustrate the applicability of secure computation compared to the classic data infrastructure available to some local governments. The project took place in a domestic, non-intelligence setting to increase the salience of potential lessons for public agencies.” Also part of the team: Nicholas R. Hart and Eric Dalton.
Jana, RAMPARTS, and the World of Tomorrow, Columbia University
Dr. David Archer gave a lecture on privacy-preserving data sharing technologies as a lecture in a Columbia University course on secure multi-party computation. This talk focused on information security, why software engineering processes are generally poor at ensuring it, deeper dives on select secure computation technologies, and descriptions of selected Galois-led developments in secure computation technologies.
Can secure computation balance data privacy and utility? GCN
Dr. David Archer published an article exploring the utility of secure computation.
“Your secretssss….we Needsss them, Precioussss”, Nike Corporation Engineering Forum
Dr. David Archer gave a talk on privacy, why it matters, and how technologists can protect it at the Nike Corporation Engineering Forum. The talk focused on current and emerging privacy risks, surveillance as the business model of the Internet, impact of privacy exploitation, and current and emerging privacy-preserving technologies to fight that exploitation.
Paper is for Writing. Brains are for Thinking. Blockchains are for…what exactly? University of Oregon Cyber Security Day
Dr. David Archer gave a talk on blockchain technology and why you need it vanishingly seldom. The talk focused on software engineering as a discipline, why it’s done poorly, and how that failure makes complex technologies (including blockchain) risky; what blockchains are, how they work, and how they compare to mature, robust technologies such as distributed databases; and why all of us should treat blockchain enthusiasm with extreme skepticism.
High Assurance Cryptography and Verifiable Elections: Three Galois Projects, VeTSS
Dr. Daniel M. Zimmerman gave an invited talk about Galois projects in high assurance cryptography and verifiable elections at the VeTSS Workshop on Verified Software.
Software Correctness and Formal Verification
Semantics-Driven Testing of the PKCS11 API, HCSS 2019
Dr. Matt Bauer and Dr. Mike Dodds gave a talk on our collaboration with Amazon Web Services to test the PKCS11 API at High Confidence Software and Systems Conference (HCSS). The talk described a model-driven testing approach to reveal high-priority bugs in PKCS11 implementations used to communicate with cryptographic devices such as hardware security modules (HSMs). The talk describes applying our approach to two PCKS11 libraries.
Automated Verification of Query Equivalence Using Satisfiability Modulo Theories, Proceedings of the VLDB Endowment
Dr. Bill Harris was part of a team that published a paper describing an algorithm that automatically determines if given SQL queries are equivalent. Also part of the team: Qi Zhou, Joy Arulraj, Shamkant B. Navathe, William Harris, Dong Xu.
ASN.1 Encoding Schemes Done Right Using CMPCT, Bx 2019
Dr. Mark Tullsen At the Eighth International Workshop on Bidirectional Transformations (Bx 2019). The talk describes an intermediate language for describing ASN.1 types as well as ASN.1 encoding schemes. Our intermediate language, CMPCT, demonstrates the elegance of using “bidirectional transformation” methods. CMPCT allows one to create arbitrary encoding schemes that are correct by construction.
The Software Analysis Workbench as a Platform for Verification Research, DSV 2019
Dr. Aaron Tomb gave an invited talk about how to use SAW as an open platform that third parties could use as a foundation for new verification research at the Workshop on Democratizing Software Verification, co-located with CAV 2019.
Functors of the World, Unite!, Compose Conference
Kenny Foner held a talk about a new, fun way of building a type system, using an elegant piece of theory called recursion schemes at Compose Conference.
A HoTT Quantum Equational Theory, QPL 2019
Dr. Jennifer Paykin was part of a team that presented a paper on equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory, at Quantum Physics and Logic 2019 (QPL 2019). The authors prove that this equational theory is sound and complete with respect to established models of quantum computation. Also part of the team: Steve Zdancewic.
Weird Machines as Insecure Compilation, FCS
Dr. Scott Moore presented a paper with Dr. Jennifer Paykin, Eric Mertens, Dr. Mark Tullsen, Luke Maurer and Benoit Razet describing how software exploitation can be viewed through the lense of secure compilation at the Workshop on Foundations of Computer Security (FCS).
Fast and secure global payments with Stellar, SOSP 2019
Dr. Giuliano Losa was part of a team that presented a paper about the Stellar payment network, including the formal verification of its core component, the Stellar Consensus Protocol at The 27th ACM Symposium on Operating Systems Principles. Also part of the team: Marta Lokhava,, David Mazières, Graydon Hoare, Nicolas Barry, Eli Gafni, Jonathan Jove, Rafał Malinowsky, and Jed McCaleb.
Stellar Consensus by Instantiation, DISC 2019
Dr. Giuliano Losa was part of a team that presented a paper on describing a theoretical analysis of consensus in the Stellar Network, and in particular the new type of permissionless quorum system that arises in the Stellar Network at 33rd International Symposium on Distributed Computing. Also part of the team: Eli Gafni and David Mazières.
Verifying the Stellar Consensus Protocol, VDS 2019
Dr. Giuliano Losa gave a talk describing the techniques employed in the formal verification of safety properties of the Stellar Consensus Protocol at the Verification of Distributed Systems workshop (VDS 2019). You can find the proof itself here. Dr. Losa also spoke about this topic at Mathematical Foundations of Programming Semantics (MFPS) XXXV.
Language Oriented Programming, WG 2.16
Dr. Iavor Diatchki gave a talk on monads at the Working Group on Programming Language Design (WG 2.16). From the abstract: “A common programming idiom in Haskell is that of a “monad”–a concept often considered to be quite difficult to understand for programmers familiar with other languages. In this talk I will introduce “monads” using terminology that is likely to be familiar to language designers, and argue that they provide an interesting way of structuring programs in any language. Furthermore, the experience of using monads in Haskell has identified a number of useful abstractions, which may form the basis for a new programming language design.”
Dependently Typed Haskell in Industry (Experience Report), ICFP 2019
Dr. David Thrane Christiansen, Dr. Iavor S. Diatchki, Dr. Robert Dockins, Dr. Joe Hendrix, and Dr. Tristan Ravitch presented Galois’s experiences using advanced Haskell type system features in the development of Crucible, a general framework for writing symbolic simulators, at the 24th ACM SIGPLAN International Conference on Functional Programming.
Bidirectional Type Checking, Compose Conference
Dr. David Thrane Christiansen presented a tutorial talk on a design technique for type systems that are straightforwardly implementable at Compose Conference.
Normalization by Evaluation, RacketFest 2019
Dr. David Thrane Christiansen gave an introduction to the technique of normalization by evaluation, for programmers used to the Racket programming language.
What About the Natural Numbers? PWLConf 2019
Dr. José Manuel Calderón Trilla gave a talk called “What About the Natural Numbers at Papers We Love Conf. The talk focused on using semantically-meaningful number systems (such as the Natural Numbers) in our programs can aid in the design of an API. The talk coincided with the 30th Anniversary of Prof. Colin Runciman’s paper “What about the natural numbers?” and used that paper as a foundation for the discussion.
The Secret Life of Not-A-Number! !!ConWest 2019
Annie Cherkaev gave a talk about a technique used by some interpreters called NaN-Boxing at !!ConWest.
Towards Verified Binary Raising, SpISA 2019
Dr. Joe Hendrix, Guanan Wei, and Simon Winwood presented their work on building verified binary reverse engineering tool that lifts x86_64 machine code into LLVM, and verifies semantics are preserved.
Hardware and Cyber-physical Systems
Secure Systems: Voting / Future Technology: SSITH, DARPA ERI Summit 2019
Dr. Joe Kiniry gave a talk outlining the goals of DARPA’s SSITH program and of Galois’s efforts to measure and evaluate the security of SSITH hardware. Dr. Kiniry explained why one of the approaches being considered to evaluate the security of SSITH hardware prototypes is public red-teaming: allowing hackers to perform their own security evaluations on mock systems with prototypes of SSITH processors. The red teaming effort was kicked off at DEF CON 2019.
RISC-V: An Open Platform for Security R&D, Real World Crypto
Dr. Joe Kiniry gave a talk on the RISC-V open-source hardware instruction set architecture and the efforts of the RISC-V Foundation at Real World Crypto 2019. Dr. Kiniry also delved into the advances in security-related R&D as it pertains to RISC-V.
21st Century Cryptography, DARPA ERI Summit 2019
Dr. Daniel M Zimmerman and William Koven gave a talk describing why getting cryptography right, especially in hardware, is difficult, and the approach Galois is taking in relevant projects. The talk focused on our hardware design approach, including synthesis from formal specifications in Cryptol and asynchronous logic, and how we are using it to mitigate power side channels in high assurance cryptographic hardware.
Correct-by-Construction Hardware Synthesis, Shonan Meeting #133
Dr. Daniel M. Zimmerman gave a talk describing the synthesis of hardware from Cryptol, the GULPHAAC project, and our approaches to cryptography and hardware. Shonan Meeting #133: Asynchronous Circuit Design and its Applications: Past, Present and Future.
Human-Machine Ethics: Experiments in Moral Responsibility, TVIW 2019
David Burke gave a talk presenting a paper at Tennessee Valley Interstellar Workshop (TVIW 2019) that addressed the question “What would it take for human beings to trust machines to help them make life-or-death decisions?” through a series of experimental scenarios, and then captured the results in a conceptual ‘congruency’ framework for thinking about moral responsibility and machine decision-making. Read the abstract here and find the paper in the link above.
Cybersecurity
Protecting Election Integrity with ElectionGuard
Dr. Joey Dodds wrote a blog post announcing the release of ElectionGuard, an SDK that enables anyone to create end-to-end verifiable (E2E-V) elections technology. ElectionGuard was developed in partnership with Microsoft. Find the main repo here, and the core ElectionGuard API SDK here.
The Art (Not Science) of Deepfakes, Nextgov
Dr. David Archer published an article that explains and explores the implications of Deepfakes.
Robust, Assured Diversity for Software Systems, RRTO Moving Target Defense Solutions
Dr. Benjamin Davis presented our automated software diversity research and variant generation technology, and how it can protect software systems by detecting and recovering from common classes of cyber attacks at Rapid Reaction Technology Office (RRTO) Moving Target Defense Solutions event. Our range of practical binary-rewriting- and compiler-based capabilities take an application to defend and automatically generate multiple variants that each behave detectably differently when under attack. Our research revealed cases where randomization-based approaches do not compose and naive layering of techniques end up negating the protections they were intended to add. Instead of randomizing blindly, we use formal reasoning to guide the layout of code and data in our variants to produce sets that maximize the chance that an attack causes observable discrepancies in variant behavior. To learn more about our approach, see this tech report on the topic.
Scientific Computing
Point Movement in a DSL for Higher-Order FEM Visualization, VIS
Dr. Charisee Chiw co-authored a paper presented at 2019 IEEE Visualization Conference (VIS). The work seeks to expose the common structure of visualization methods, apart from the specifics of how the fields being visualized are formed. Also part of the team: John Reppy
Data Analysis and Machine Learning
Artificial Intelligence and Cybersecurity Workshop
Dr. John Launchbury led the Artificial Intelligence and Cybersecurity Workshop with Patrick McDaniel. The workshop’s aim was to assess the current and future research challenges and opportunities at the intersection of cybersecurity and artificial intelligence and to identify key research gaps. Find the briefing slides here.
An Inductive Synthesis Framework for Verifiable Reinforcement Learning, PLDI 2019
Dr. Stephen Magill and Dr. He Zhu were part of a team that published a paper on making assurance guarantees for machine-learning applications. The paper considers “how formal verification techniques developed for traditional software systems can be repurposed for verification of reinforcement learning-enabled ones, a particularly important class of machine learning systems.” Watch the talk on the paper here. Also part of the team: Zikang Xiong and Suresh Jagannathan at Purdue University.
Mental Health
How Can I Academia When My Brain Can’t Even? Mental Health in Grad School and Beyond, PLMW 2019
Kenny Foner gave an invited talk about mental health in academia at the Programming Languages Mentoring Workshop at SPLASH 2019, telling the story of their own experiences of mental illness within and after grad school, and giving strategies and resources for future researchers to support themselves and others in the world of academia and beyond.
Contract Award Announcements
Galois Awarded $8.6 Million DARPA Contract To Build Cyber Reasoning Tool that Discovers Security Vulnerabilities: Galois partners with Harvard University and Trail of Bits to build scalable and more cost-effective tools that identify hard-to-find vulnerabilities.
Galois Awarded $15M IARPA Contract To Expand Government, Commercial Use Of Privacy-Preserving Technology: Project for IARPA’s HECTOR Program focused on making secure computation accessible to data scientists, other programmers who are not experts in cryptography.
Spin-out News
Muse Dev: We spun out Muse Dev, a startup developing tools that help you find critical bugs early in the development process. Muse Dev is serving a number of early, private beta customers.
The Muse Dev team held numerous talks, including
- Shifting QA Left: Emerging Trends in Code Quality and Security Automation at DOES 2019,
- Code + AI: Will Robots Take Our Coding Jobs? at GOTO 2019, and
- A data-driven look at practices behind exemplar open source projects at Github Universe.
Tangram Flex: Tangram Flex grew significantly in 2019. The team also launched theFramework, a series of articles that delve into systems engineering, security and safety, and integration.
Tozny: Tozny launched TozID, a privacy-first identity management solution with privacy and end-to-end encryption built in.
Other News
Life as a Galois Project Lead: We continue to share what working at Galois is like on Life at Galois. This year we explored what being a Project Lead is like at Galois.
Girls Who Code Chapter: At this year’s Grace Hopper celebration, we didn’t bring Galois branded swag, and instead used the funding to support a chapter of Girls Who Code in Dayton, Ohio. The chapter purchased programmable robot kits and is tackling a number of projects in teams.
Parental leave: We revised our approach to parental leave and increased it to 16 weeks.
Increased focus on a more inclusive workspace: We started organizing company lunches for under-represented groups in computer science. We also started an action group on proactive changes the company can make to be more inclusive of current and future Galwegians regardless of race, gender, sexuality, religion, or disability.
More inclusive company activities: We started organizing company activities focused on an expanding variety of interests for mental health and relaxation. Examples include paint nights, pumpkin decorating, gingerbread houses, and a craft corner.
Tech Talks: Galois organized and hosted 8 public tech talks on a variety of topics.
James Edmondson joins Galois as Principal Scientist: We welcomed Dr. James Edmondson to the Galois team as Principal Scientist. Dr. Edmondson’s research focuses on the command and control, visualization, determinism, and trust of distributed artificial intelligence in robotics.
IEEE Micro Best Paper Award: Dr. Georgios Dimou was awarded “Best Paper” for Loihi: A Neuromorphic Manycore Processor with On-Chip Learning.
Washington Technology 2019 Industry Innovators: Washington Technology named Galois one of the winners of the Industry Innovator Awards, which aims to show the breadth and depth of capabilities of government contractors.
Reboot Leadership Awards – Influencer: Joe Kiniry: Dr. Joe Kiniry was recognized by SC Magazine for his work in collaboration with DARPA, Microsoft, and the State of Colorado.
Reboot Leadership Awards – Privacy Leads: David Archer: Dr. David archer was recognized by SC Magazine for his work on secure computation with DARPA, The Census Bureau, DHS, and IARPA.
Continuous Formal Verification of Amazon s2n – honorable mention: The paper that details our initial work with Amazon Web Services to integrate formal methods in the development workflow for security-critical software at AWS was selected for an honorable mention in the Best Scientific Cybersecurity Paper Competition sponsored NSA’s Research Directorate. Read the paper here.
Functional Programming competition: We sponsored a competition for the students in the introductory Functional Programming class. Browse the student projects here.
Press Highlights
And now a Bicycle for None: Dr. Georgios Dimou spoke with the New York Times about neuromorphic chips with on-chip learning capabilities that are designed to imitate the network of neurons in the brain.
DARPA to Bring its Smart Ballot Boxes to DEF CON for Hacking: Dr. Daniel Zimmerman was interviewed by Dark Reading about the kick-off of the public red-teaming effort to evaluate the security of DARPA SSITH processor prototypes.
Microsoft offers software tools to secure elections: The Associated Press reported on ElectionGuard, the software development kit that enables end-to-end verifiable elections technology, developed in partnership with Microsoft.
Building Security Into RISC-V Systems: Dr. Joe Kiniry was interviewed as part of a panel of experts on Building Security into RISC-V Hardware in Semiconductor Engineering.
Other Community Engagements
Dr David Archer served as co-editor for the UN Privacy Preserving Techniques Handbook
Dr. John Launchbury
- served on the Forum on Cyber Resilience of the National Academies of Sciences, Engineering, and Medicine
- served as a steering committee member for DARPA’s Information Science and Technology (ISAT) Study Group
- served on the steering committee for High-confidence Software and Systems (HCSS)
- served as a member of the Working Group on Functional Programming (WG2.8)
- participated in Computing Community Consortium’s Assured Autonomy Workshop
- served as a distinguished expert in the selection committee of NSA’s Best Scientific Cybersecurity Paper Competition
Dr. Iavor Diatchki
- served on the program committee for International Symposium on Practical Aspects of Declarative Languages (PADL 2020)
- continued to serve on the Glasgow Haskell Compiler (GHC) steering committee
- served as chair of the Haskell Symposium steering committee
Dr. David Thrane Christiansen and Dr. Iavor S. Diatchki held a one-day introduction to Cryptol and SAW at the 24th ACM SIGPLAN International Conference on Functional Programming
David Thrane Christiansen served on the program committee for the 2019 Workshop on Metaprogramming (META 2019) at SPLASH
Dr. Charisee Chiw organized an outreach event with a local high-school Robotics team. About 20 students from St. Marys spent half a day at the Galois office. Various Galweigans gave short technical talks covering topics like quantum computing, creating safe voting machines, 3D modeling design, and domain-specific languages. We also had an open discussion about various engineering topics and career paths.
Dr. Scott Moore
- served on the program committee of the Workshop on Foundations of Computer Security Program (FCS 2020)
- served on the program committee of Computer Security Foundations Symposium (CSF 2020)
Dr. Jennifer Paykin
- served on the program committee of the International Conference on Functional Programming (ICFP 2019)
- Served on the programming committee of the Workshop on Programming Languages for Quantum Computing (PLanQC 2020).
Dr. Joe Hendrix served as chair of the Workshop on Satisfiability Modulo Theories (SMT 2019), and served on the FMCAD 2019 program committee.
Dr. Georgios D. Dimou served on the program committee for ASYNC Symposium
Dr. Aaron Tomb served as a committee member for the Workshop on Satisfiability Modulo Theories (SMT 2019)
Dr. Aaron Tomb and Dr. Daniel M. Zimmerman participated in High Assurance Systems Engineering (HASE) workshop.
Dr. Daniel M. Zimmerman gave the keynote talk at E-Vote-ID about the evolution of Galois and Free & Fair’s research efforts in the elections space.
Dr. David Archer and Meckler Izaak gave a workshop on formal verification for zero-knowledge systems at ZKProof 2019
Dr. David Archer gave a keynote talk on how and why to deploy continuous formal verification as an assurance method for complex ASIC/FPGA products at Modern Formal Verification in Practice, Verification Sciences & Engineering Workshop
Dr. Joe Kiniry gave a talk at a panel on DARPA’s POSH and IDEA programs.
Software Releases
Cryptol: We released two new versions of Cryptol (2.7.0 and 2.8.0). Feature highlights include adding support for test vector creation, useful for generating tests from a trusted Cryptol specification to apply to an implementation written in another language, and a variety of small changes to the language that make it more convenient to express common patterns.
Software Analysis Workbench: We released two new versions of SAW (0.3 and 0.4). In 0.3, Java and LLVM verification was overhauled to use the new Crucible symbolic execution engine. In 0.4, we significantly improved functionality along with major bug fixes.
ElectionGuard SDK: In collaboration with Microsoft, we released ElectionGuard, an SDK that enables anyone to create end-to-end verifiable (E2E-V) elections technology. Find the main repo here, and the core ElectionGuard API SDK here.
Matterhorn: Galois continues to maintain and improve our open-source Mattermost terminal client.