2017 brought continued growth in concern about the trustworthiness of computing systems. The breadth of our work at Galois has grown correspondingly. We opened a third office in Dayton, Ohio, grew past 70 employees, and continue to actively hire. We are grateful to our partners and clients that have helped us successfully develop the projects and intellectual contributions highlighted below. We’re excited to continue the effort with you in 2018.

Overview

In cyber-physical systems security and reliability research, we continued our work on both ground and air vehicles. We published an in-depth look at automotive vulnerabilities and approaches to secure automotive software in a special issue of IEEE Software. We also presented preliminary work on formally verifying a vehicle-to-vehicle (V2V) messaging system, and on extending and retrofitting UxAS, a software system from the Air Force Research Laboratory (AFRL) for multi-UAV cooperative decision making.

We released our first report on applying formal methods to autonomous systems that incorporate neural-network-based reinforcement learning. Our efforts showed that, in combination, our formal methods approach enabled policy training with dramatically less data.

Our work with Amazon to formally verify core components of the s2n encryption library continued to play a role in making essential software more secure. It is being leveraged by other important open source libraries, and we also gave a number of presentations on the process of automation and continuous integration of formal verification techniques in use with s2n.

We continued to work on secure computation, the groundbreaking process of using sensitive, encrypted data without decrypting it. This year, our work focused on making these processes faster and more accessible.

Our work on automatically detecting and preventing Distributed Denial of Service (DDoS) attacks evolved into more general network flow analysis and anomaly detection. At the Canadian ISP summit, we presented approaches that assist administrators by automating the detection of unusual patterns and anomalous flows, and the search for known issues that might cause them.

More generally in cybersecurity, we published articles on government in-depth defense, and released tech reports on reducing return-oriented programming (ROP) exploits, a mechanism that allows attackers to string together small snippets of existing executable code in order to exploit programs.

We announced three contract awards from the U.S. Air Force, Navy, and the Intelligence Advanced Research Projects Activity (IARPA), and won many more which we will be announcing in 2018. We also actively contributed to the public conversation around cybersecurity and software assurance through a number of interviews and articles in the press.

Below you will find more detail on those contributions, organized by field. From all of us at Galois, we wish you a happy and productive new year.

High-assurance Cryptography

Privacy Technologies for Controlled Information Sharing in Coalition Operations, Best Paper award at KSCO

Dr. Stephen Magill and Dr. David Archer were part of the team that published a paper on improving secure information sharing at Knowledge Systems for Coalition Operations (KSCO 2017). The paper considers how advanced privacy technologies can enable improved information sharing among coalition partners by both providing increased control over how information is used or released, and enabling principled characterizations of the impact of individual and cumulative sharing activities. It describes this work in the context of a humanitarian aid and disaster relief scenario, showing how the technologies can enable significantly increased and informed sharing. Also part of the team: Karen Myers, Tim Ellis, Tancrède Lepoint, Ronald A. Moore, Grit Denker, Steve Lu, Rafail Ostrovsky.

Assuring Crypto-code with Automated Reasoning, QCon 2017

Dr. Aaron Tomb gave a talk at QCon 2017 where he described the capabilities and operation of open source tools that allow developers to conclusively and largely automatically determine whether a low-level cryptographic implementation exactly matches a higher-level mathematical specification. Dr. Tomb used Galois’s collaboration with Amazon to illustrate how these tools were integrated into the continuous integration system of their s2n implementation of TLS. See the source link for the slide deck and video of the presentation.

Attribute-based Key Exchange with General Policies, TPMPC 2017

Dr. Alex Malozemoff gave an invited talk on attribute-based key exchange at the Theory and Practice of Multi-Party Computation Workshop (TPMPC 2017). Attribute-based key exchange allows the establishment of a secure channel between a server and client if and only if the client satisfies some underlying policy.

Julia for Fully Homomorphic Encryption: Current Progress and Challenges, JuliaCon

Dr. José Calderón gave a presentation on Julia extensions for Fully Homomorphic Encryption at JuliaCon 2017. In the talk, Dr. Calderón introduced a Julia module, Fhe.jl, which supports running Julia functions over an FHE-encrypted data set. This is done by using symbolic execution to convert a Julia function into its circuit representation, which we then evaluate over the encrypted data. The work is part of Galois’s RAMPARTS project.

Jana – Private Data as a Service, HCSS 2017

Dr. David Archer gave a talk on Jana, a privacy preserving data service in which data is encrypted at all times, at High Confidence Software and Systems (HCSS 2017). The project is part of Galois’s efforts on DARPA Brandeis.

Faster Secure Two-party Computation in the Single-execution Setting, Eurocrypt 2017

Dr. Alex J. Malozemoff was part of a team that published and presented a paper introducing a two-party computation protocol at Eurocrypt 2017. The paper proposes a new protocol for two-party computation, secure against malicious adversaries, that is significantly faster than prior work in the single-execution setting Also part of the team: Xiao Wang, Jonathan Katz.

5Gen-C: Multi-input Functional Encryption and Program Obfuscation for Arithmetic Circuits, CCS 2017

Brent Carmer and Dr. Alex J. Malozemoff were part of a team that published a paper on cryptographic program obfuscation at the ACM Conference on Computer and Communications Security (CCS 2017). From the abstract: “In this work, we explore in detail cryptographic program obfuscation and the related primitive of multi-input functional encryption (MIFE). In particular, we extend the 5Gen framework (CCS 2016) to support circuit-based MIFE and program obfuscation, implementing both existing and new constructions. We then evaluate and compare the efficiency of these constructions in the context of PRF obfuscation.” Also part of the team: Mariana Raykova.

Revolution and Evolution: Fully Homomorphic Encryption, US Cybersecurity Magazine, vol. 5, no. 16, 2017

U.S. Cybersecurity Magazine published an introduction to fully homomorphic encryption by Dr. David Archer. The article introduces the concept of computing on data while it remains encrypted and presents the current state of the technology. You can find the article on www.uscybersecurity.net or on the Galois blog here.

Homomorphic Encryption Standardization Workshop, White Papers, Microsoft Research

Dr. David Archer and Dr. Alex J. Malozemoff participated in Microsoft Research’s Homomorphic Encryption Standardization Workshop, where they co-authored to two white papers:

• Applications of Homomorphic Encryption, and
• A Standard API for RLWE-based Homomorphic Encryption.

Applying NIST’s New Privacy Risk Management Framework, HCSS 2017

Isaac Potoczny-Jones, CEO of Galois spin-off Tozny, gave a presentation on NIST’s Privacy Risk Management Framework at High Confidence Software and Systems (HCSS 2017). In the talk, Potoczny-Jones gave an overview of NIST’s Privacy Framework and related standards (800–53, 800–63); described the implementation of a product, E3DB, based on these standards; and gave an in-depth review of the E3DB’s cryptographic approach and how it supports privacy.

Data Privacy Issues in Distributed Security Monitoring Systems

Dr. David Archer co-authored a book chapter titled “Data Privacy Issues in Distributed Security Monitoring Systems” in Security and Privacy in Cyber-Physical Systems: Foundations, Principles, and Applications.

Software Correctness and Formal Verification

Formal Methods and the KRACK Vulnerability

Dr. Joey Dodds, with input from other Galwegians, weighed in on the WPA2 KRACK vulnerability that was revealed to enable a range of attacks on the protocol. The article covered some of the concerns around standards and formal verification presented in the original paper with the goal of providing insights into real-world cryptography verification.

Abstract Interpretation at Galois, N40AI

Dr. Aaron Tomb gave a talk on abstract interpretation at Galois at the Next 40 Years of Abstract Interpretation (N40AI) series at POPL 2017. From the abstract: “Abstract interpretation has been part of Galois since its inception, even so far as to influence the original name of the company: Galois Connections. Aaron Tomb will talk about how Galois has used abstract interpretation in practice over the last decade and a half, and describe some long range ideas for what might make the techniques even more useful over the next four decades.”

Type Theory in the Software Analysis Workbench (SAW), TTT 2017

Dr. Aaron Tomb gave an invited talk on Galois’s Software Analysis Workbench (SAW) and its use of dependently typed features at Type Theory Based Tools (TTT) series at POPL 2017. Dr. Tomb described the basic structure and capabilities of SAW, including some examples of widely used cryptographic code that we have verified with it. He also described the features of SAW’s intermediate language, including details about how it uses the dependently typed features.

Proving Amazon’s s2n Correct, HCSS 2017

Dr. Joey Dodds presented our ongoing work to formally verify components of Amazon’s s2n TLS encryption library at High Confidence Software and Systems (HCSS 2017). Dr. Dodds gave an overview of the process by which verification is being done, particularly focusing on automation and continuous integration of the verification tools. The verification runs automatically with each code change, often keeping the proof intact despite changes to the software. For more information on the project, visit the project page on the Galois website.

Proving Functional Correctness with the Software Analysis Workbench (SAW), AFRL S5

Dr. Aaron Tomb gave a talk on using SAW to prove functional correctness at the Air Force Research Laboratory’s Safe and Secure Systems and Software Symposium (S5 2017). The talk used the verification of s2n components to demonstrate current capabilities.

Modular Model-Checking of a Byzantine Fault-Tolerant Protocol, NASA Formal Methods Symposium 2017

Dr. Lee Pike and Dr. Benjamin Jones presented a paper on model checking distributed, fault tolerant systems at the NASA Formal Methods Symposium. The paper presented a general framework for modeling distributed, fault-tolerant systems and walked through a case study, modeling variations on the Oral Messages algorithm that vary in their timing model, node behavior, and fault model.

Laziness Boxes You In, POPL 2017

Dr. José Calderón and Dr. Stephen Magill presented a paper at POPL 2017 on inferring information leakage via forced thunks. The talk and paper gave an overview on representing sensitive information as lazy values to give bounds on the amount of information leakage from a program.

Starling: Lightweight Concurrency Verification with Views, CAV 2017

Dr. Mike Dodds presented a paper at the Computer Aided Verification (CAV 2017) conference on verifying concurrent programs. Dr. Dodds also presented similar work at the Mathematical Foundations of Programming Semantics XXXIII (MFPS 2017) and at NII Shonan Meeting Seminar 100. From the abstract: “Starling is a lightweight, automated tool for verifying racy concurrent algorithms. Starling proofs are written in an abstracted Hoare-logic style, and converted into terms discharged by a sequential solver (for example, Z3). Starling is built on the Views framework, an abstract form of separation logic. In this talk I’ll describe how we specialise the Views framework into a simple, generic verification tool, and how we can apply this approach to verify complex pointer programs.”

High-assurance Cyber-physical Systems

Programming Languages for High-Assurance Vehicles, LangSec Workshop, IEEE Security & Privacy (video)

Dr. Lee Pike presented our experiences in synthesizing a fully featured autopilot from embedded domain-specific languages (EDSLs) hosted in Haskell at the LangSec Workshop at IEEE Security & Privacy. The autopilot was built for the DARPA High-Assurance Cyber-Military Systems (HACMS) program. Full video of the invited talk can be found here.

Secure Automotive Software: The Next Steps, IEEE Software, Volume 34, Issue:3

Dr. Lee Pike, Jamey Sharp, Dr. Mark Tullsen, Patrick C. Hickey, and James Bielman published an article on automotive vulnerabilities on a special IEEE Software issue focused on automotive software. The article reviews research that revealed pervasive software vulnerabilities in modern automobiles, explores the challenges that the automotive industry faces that can impede improved software security, and discusses four general approaches to secure automotive software systems: compile-time assurance, runtime protection, automated testing, and architecture security. You can find a pre-copyedited version of the paper here.

Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System, ESCAR USA 2017 and HCSS 2017

Dr. Mark Tullsen presented a paper at ESCAR USA 2017 on formally verifying a V2V messaging system. The paper was authored by Nathan Collins, Mark Tullsen, Dr. Aaron Tomb and Dr. Lee Pike. Dr. Tullsen also presented similar work at High Confidence Software and Systems (HCSS 2017); find the abstract here.

Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System, CPS V&V I&F Workshop 2017

Dr. Stephen Magill presented work on verifying a V2V messaging system at the Cyber Physical Systems Verification & Validation: Industrial Challenges & Foundations Workshop (CPS V&V I&F 2017). The talk presented the generation and formal verification of an ASN.1 encoder/decoder pair, implemented in C, using the High-Assurance ASN.1 Workbench and the Software Analysis Workbench.

Improving Communication Security of Open Source UAVs: Encrypting Radio Control Link, ICUAS USA 2017

Michal Podhradsky was part of a team that published a paper on securing radio control links in open-source UAV software at the 2017 International Conference on Unmanned Aircraft Systems (ICUAS USA 2017). The paper proposes an implementation of an encrypted radio control (RC) link that can be used with a number of popular RC transmitters, using the ArduinoLibs, Galois Embedded Crypto library and openLRSng open-source radio project. Also part of the team: Nathan V. Hoffer and Calvin Coopmans.

A Commitment Logic for Reasoning about Trust in Complex Systems, HCSS 2017

David Burke gave a presentation on commitment logic at High Confidence Software and Systems (HCSS 2017). Mr. Burke presented a framework based on commitment logic to reason about the trustworthiness of human-machine collectives (humans and AI agents).

Memory Safety of UxAS Tasks / Retrofitting UxAS with Rust, AFRL S5 2017

Adam Foltzer presented work on using Rust to rewrite parts of UXaS, a software system for multi-UAV cooperative decision-making, at Safe and Secure Systems and Software Symposium (S5 2017) organized by the Air Force Research Laboratory (AFRL).

Breaking the Human-Robot Deadlock: Surpassing Shared Control Performance Limits with Sparse Human-Robot Interaction, RSS 2017

Dr. Pete Trautman published a paper in Robotics: Science and Systems (RSS 2017) on human-machine teaming and interaction. The paper introduced generalized shared control, and proved that it optimizes human and robot agreement and intent under arbitrary ambiguity in a computationally efficient manner.

Sparse Interacting Gaussian Processes: Efficiency and Optimality Theorems of Autonomous Crowd Navigation, Conference on Decision and Control 2017

Dr. Pete Trautman presented a paper about autonomous crowd navigation in Conference on Decision and Control (CDC 2017). The paper studies “the sparsity and optimality properties of crowd navigation and find that existing techniques” are lacking. It then diagnoses the cause of the deficiencies and introduces a novel solution.

Probabilistic Versus Linear Blending Approaches to Shared Control for Wheelchair Driving, International Conference on Rehabilitation Robotics, 2017

Dr. Pete Trautman was part of a team that published a paper on shared control for wheelchair driving at the International Conference on Rehabilitation Robotics, 2017. Also part of the team: C. Ezeh, L. Devigne, V. Bureau, M. Babel and T. Carlson. Dr. Trautman was also part of a team that published a paper on wheelchair shared control approaches at the IEEE International Conference on Systems, Man, and Cybernetics, 2017.

Dr. Trautman also published a number of other papers on the topics of shared control:

• Generalized Shared Control versus Classical Shared Control: Illustrative Examples, Pete Trautman.
• Manifold Relevance Determination: Learning the Latent Space of Robotics, Pete Trautman.
• Integrating High and Low Level Path Planning, Pete Trautman.

Cybersecurity

Tech Report: Systems Support for Hardware Anti-ROP

Jason Dagit, Dr. Simon Winwood, Getty Ritter, Jem Berkes, and Dr. Adam Wick were part of a team that published a tech report on hardware extensions and software modifications that reduce return-oriented programming (ROP) exploits, a mechanism whereby an attacker can string together small snippets of existing executable code—known as gadgets—in order to exploit programs without injecting new bits of code. Also part of the team: Andrew White and George Coker, NSA.

Tech Report: Code Re-use Attacks and their Mitigation

Jason Dagit, Dr. Simon Winwood, Getty Ritter, Jem Berkes, and Dr. Adam Wick published a tech report that provided a brief summary of notable attacks and mitigations with a focus on return-oriented programming (ROP).

Provenance of Computation Meets Persistent Threat Detection: A Progress Report, TaPP 2017

Dr. David Archer gave an invited talk on detecting advanced persistent threats (APTs) at the 9th International Workshop on Theory and Practice of Provenance (TaPP 2017). Dr. Archer described our approach to detecting APTs using a combination of statistical anomaly detection and computational provenance exploration, walked through the architecture of our detection system, described the sensor data model we use as input to our analysis, explored our anomaly detection and provenance computation methods, and presented preliminary results from a recent adversarial engagement on real systems under realistic attack.

Network Information Sharing: One World, One Love: Sharing Intel to Make the Network Safer, Oregon CyberSecurity Summit

Galois co-organized the Oregon CyberSecurity Summit, at which Dr. David Archer presented our approach to privacy-preserving analysis of network compromise that allows for sharing indicators of compromise between distinct networks without revealing the data that led to establishing those IoCs.

DDoS Defense with a Community of Peers (3DCoP), Flocon 2017

Jem Berkes gave a presentation on defending against DDoS attacks using collaborative techniques at Flocon 2017. In the presentation, Mr. Berkes gave an overview of 3DCoP, a Galois project that aims to use information sharing for automatic DDoS defense. He also presented 3DCoP at DHS S&T R&D Showcase and Technical Workshop. You can find that presentation here.

I Want Your Flows To Be Lies, Flocon 2017

Dr. Adam Wick gave a presentation at Flocon 2017 on using cyber deception to mask flow data in a network in order to thwart attackers that are looking to gain a foothold on a network. The talk also illustrated how Galois’s CyberChaff and Prattle can be used to mask the real flows in a network.

Gossiping for Good: The Benefits of Automatic Collaboration, Canadian ISP Summit

Dr. Adam Wick gave a talk on detecting problems within networks through flow-data analysis at the Canadian ISP summit. The talk presented a tool that assists administrators by automating the detection of unusual patterns and anomalous flows, and the search for known issues that might cause them.

End-to-end Information Flow Control for Hybrid Android Applications, IEEE MoST (Mobile Security Technologies) 2017

Dr. Andrey Chudnov was part of a team that presented a paper on enforcing security in hybrid Android applications at Mobile Security Technologies (IEEE MoST 2017). The paper explored how to leverage static analysis of Android/Java and dynamic analysis of Javascript to enforce information flow policies in such applications. Also part of the team: Julian Sexton and Dr. David Naumann.

With Government Cyber Defense, Sometimes It’s Best to Give up Hope, Federal News Radio

Dr. Adam Wick published an opinion piece on Federal News Radio on ways that government entities should approach cyber defense. From the introduction: “As counterintuitive as that may sound, there is no magic bullet that will solve all our cybersecurity challenges. A sufficiently motivated and capable adversary will get around our defenses, given enough time. The question then becomes: How can we tax that motivation, or increase the cost of these attacks? What emerging areas of cybersecurity should government decision makers focus on to extend the range and capability of our deterrents? Three areas in particular warrant government attention: cyber deception, defense in-depth and formal verification.”

Data Analysis and Machine Learning

Tech Report: Applying Formal Methods to Reinforcement Learning

Dr. He Zhu and Dr. Stephen Magill published a tech report on formal methods guided testing of autonomous systems. In particular, the report looks at closed-loop control systems that incorporate neural network based reinforcement learning components.

Using Formal Methods to Reason About Neural Network Based Autonomous Systems, AFRL S5

Dr. Stephen Magill presented work by Dr. He Zhu and Dr. Magill on using formal methods to reason about machine learning at the Air Force Research Laboratory’s Safe and Secure Systems and Software Symposium (S5 2017).

GraPPa: Spanning the Expressivity vs. Efficiency Continuum, PPS 2017.

Dr. Eddy Westbrook, Dr. Chad Scherrer, Nathan Collins, and Eric Mertens presented a paper on GraPPa, the Galois Probabilistic Programming Language, at the workshop on probabilistic programming semantics series at POPL 2017.

Announcements, Events, and Releases

Galois organized 7 public tech talks on a wide range of topics. Visit the tech talks page for the complete list.

Galois Awarded Air Force Grant for Advanced Cyber Deception Technology. The $750,000 grant from the Air Force Research Lab (AFRL) aims to develop a new, advanced network cyber deception technology, Prattle, that generates realistic traffic to tag adversaries monitoring network activity, mislead them about things they may have learned, and cause them to make mistakes that increase the likelihood of detection.

DARPA, Galois Launch Benchmark Challenges to Prvent Software ‘Reverse Engineering’. The challenges invited competitive submissions able to break the security of program obfuscation technology designed to prevent software ‘reverse engineering.’

Galois Awarded $2.7 Million Navy Contract to Develop New Cyber Resilience Capability. The ONR-funded project focuses on protecting real-time and embedded military software systems by making them resilient to attack. The project aims to harden control systems by using binary rewriting to add brittleness to legacy binaries.

Galois Awarded $1 Million IARPA Contract to Improve Security of Data Computation.  The project explored advancing the practical ease of programming, optimizing compilers, and high-performance libraries for fully homomorphic encryption.

Galois launched the first office in Dayton, OH, co-located with the Nucleus incubator, Mile Two, and the Wright Brothers Institute.

Galois established Discussions on Trustworthy Systems (DOTS), a periodic gathering of individuals and organizations interested in closing the gaps on cyber vulnerabilities in embedded systems, in collaboration with the Armed Forces Communications and Electronics Association (AFCEA). The first gathering featured talks from the University of Illinois, Galois, and AFRL. The second gathering featured talks from Purdue University, Aurora Flight Sciences, and AFRL Autonomy Initiative, and can be found on YouTube here.

Our collaboration with Amazon Web Services to formally verify parts of s2n continued to make essential software more secure. From the Amazon Web Services’ blog post: “Earlier this year, with Galois, we completed a proof of our implementation of AES_CTR_DRBG, and formally verified that our code in s2n is equivalent to the written specification. Recently, both the OpenSSL and glibc projects have been looking to replace their random number generators. They, too, are going with AES_CTR_DRBG, based in some part on the work in s2n and the availability of formal verifications that can be applied to code. That’s pretty sweet.”

Galois presented work on high-assurance, formally verified, end-to-end systems and formally verified trusted boot for RISC-V at the 7th RISC-V Workshop.

Galois spin-off Tozny launched InnoVault, an end-to-end encryption toolkit for developers.

Galois spin-off Free & Fair was awarded a contract by the State of Colorado to develop a risk-limiting audit system that was used in the November 2017 general election, marking the first time that risk-limiting audits have been conducted on a regular, statewide basis in the U.S. For more information, see Free & Fair’s page on RLAs or check out this story on the auditing process.

Free & Fair attended and presented at SXSW, with the aim of providing material and education on elections technology, potential vulnerabilities, and mitigation. Following SXSW, Free & Fair shipped a election education technology platform called Election Security 101.

Free & Fair co-sponsored and helped organized and run the annual Elections Verification Network Symposium and Conference in Washington, D.C. and the Global Election Technology Summit in San Francisco.

Galois released ddosflowgen, an open-source tool that simulates DDoS attacks.

Galois released Matterhorn, a terminal client for the Mattermost chat system.

Galois released Cryptol 2.5.0, with major improvements to the interpreter and type checker.

Dr. Mike Dodds joined Galois as Principal Investigator.

Dr. John Launchbury re-joined Galois as Chief Scientist.

Press Coverage Highlights

• Loose Lips may better Air Force security with ‘Prattle’, Federal News Radio
• Air Force goes after cyber deception technology, Network World
• Crypto-currency software emerges as tool to block cyber attacks, Bloomberg Business Week
• Galois wins $5.6m contract to help defeat reverse engineering threats, Washington Technology
• Northwest universities evaluating new approach to DDoS attacks, University Business
• How to make Fully Homomorphic Encryption “practical and usable”, Network World
• Privacy and Encryption Above the Data: Interview with Dave Archer, Fast Forward Labs (Interview with David Archer)
• EDUCATION ENCRYPTION BILL DROPS, Politico, (Quotes David Archer)
• The Security Panacea: Striking Balance with Usability, Tyntec (Interview with Isaac Potoczny-Jones)
• Why next gen vehicles should consider security from the start, StateScoop (Interview with Isaac Potoczny-Jones)
• Galois elections technology spin off, Free & Fair, saw broad coverage and interviews, from publications such as Route Fifty, Federal Computer Week, and the New York Times. For a complete list of coverage, see the news section on freeandfair.us.

Program Committees, Reviewing, Guest Editing

• Iavor Diatchki, Program Committee Chair for Haskell Symposium 2017.
• Trevor Elliott, external reviewer for Haskell Symposium 2017 and FMCAD 2017.
• Eric Mertens, external reviewer for Haskell Symposium 2017.
• Dr. Alex J. Malozemoff, External reviewer for Crypto 2017, ACM CCS 2017, TCC 2017, LatinCrypt 2017, IndoCrypt 2017.
• Dr. Stephen Magill, HCSS Program Committee.
• Dr. Lee Pike, FMCAD Program Committee.
• Dr. José Calderón, chair of SIGPLAN Research Highlights Committee; video chair for ICFP 2017; external reviewer for Haskell Symposium 2017.
• Dr. Andrey Chudnov, reviewer for the Formal Aspects of Computing journal.
• Dr. Pete Trautman, Chair of “Autonomous Robots 1” session at Conference on Decision and Control.
• Dr. Adam, Track, Host of Modern CS in the Real World at QCon 2017.
• Dr. Scott Moore, DLS and ACM SIGSAC PLAS Program Committees.
• Dr. Mike Dodds, ECOOP 2017 Program Committee.