High Assurance Software Jump to section
Secure Computation Jump to section
Security Analytics Jump to section
Trusted Autonomy Jump to section

Center for Secure and Resilient Systems (CSRS)

Part of HRL's Information and Systems Sciences Laboratory, the Center for Secure and Resilient Systems (CSRS) is devoted to development of novel tools and techniques for creation and analysis of complex systems capable of maintaining their functionality in unpredictable adversarial environments.

At CSRS, we are building resilience and security techniques on firm theoretical foundations, drawing from formal methods and logic, cryptography, distributed systems, graph theory, network science, and machine learning. We capture these techniques in new algorithms, protocols and tools, which we then use to build practical systems in multiple domains, including heterogeneous distributed systems and cyber-physical systems. We believe that with proper tools and frameworks, construction of resilient secure systems can be made efficient and practical, and the resilience and security does not have to come at a price of increased implementation cost, or reduced performance.

CSRS is committed to being a part of the broader research community; we actively collaborate with both academic and industry researchers.


High Assurance Software

We are using a range of formal methods techniques and formal reasoning tools for production of software that is equipped with mathematical proofs stating that the software does what it is supposed to, and nothing else. In our work we are particularly targeting software for cyber-physical systems, such as autonomous ground vehicles and SCADA-type systems.

As part of this work, we are developed a mixed-assurance software toolchain (MAST) capable of analyzing and integrating in a consistent way mixed assurance software components produced by a combination of different tools and techniques.

We are also looking into automated synthesis of software for complex cryptographic protocols

Current and Recent Collaborators
  • Boeing
  • Carnegie Mellon University (CMU)
  • Commonwealth Scientific and Industrial Research Organisation (CSIRO) / Data61
  • Galois, Inc
  • Kestrel Institute
  • Massachusetts Institute of Technology (MIT)
  • Princeton University
  • QuviQ
  • Rockwell Collins
  • SpiralGen
  • SRI
  • Stevens Institute of Technology
  • University of Illinois at Urbana-Champaign (UIUC)
  • University of Minnesota
  • University of Pennsylvania
  • US Army Tank Automotive Research and Development Engineering Center (TARDEC)
  • Yale

Secure Computation

We have developed a number of secure and privacy-preserving distributed protocols that far exceed the previous state of the art in their performance and/or security characteristics. We are applying these protocols to development of secure and privacy-preserving distributed systems, with applications including cloud control and secure biometrics.

Current and Recent Collaborators
  • University of California Los Angeles (UCLA)
  • University of California Irvine (UCI)
  • University of Maryland, College Park (UMD)

Security Analytics

We are developing tools and techniques that leverage advances in network science, data analytics, and machine learning to protect networked assets from sophisticated cyber-attacks by identifying subtle patterns in system data and network traffic that indicate their presence and reveal their activities. We have successfully applied this approach to the challenging problem of detecting and mitigating sophisticated attacks on mobile ad-hoc wireless networks.

We are also investigating techniques to protect personal assets from social engineering attacks by mining and analyzing social media and other online sources of data to model, predict, and manipulate attackers into revealing information that can be used for attribution and mitigation.

Current and Recent Collaborators
  • Northeastern University
  • Harvard University
  • University of Miami

Trusted Autonomy

We are engaged in a number of research projects aimed at developing techniques for being able to establish trust in complex autonomous learning-enabled systems, such as those involved in autonomous driving. This includes developing tools and techniques for formal design and analysis of learning-enabled components, learning-enabled systems, and systems of systems. This also includes investigating machine learning techniques that can provide strong assurance of absence of unintended behaviors, even in certain adversarial settings.

Current and Recent Collaborators
  • Carnegie Mellon University (CMU)
  • University of California, San Diego (UCSD)
  • University of Illinois at Urbana-Champaign (UIUC)
  • Runtime Verification, Inc (RV)
  • University of California Santa Barbara (UCSB)

Current and Recent Projects

Assured Autonomy using Expressive Assurance Case Toolkit (AA-ExACT)

As part of the DARPA Assured Autonomy (AA) program, we are addressing the challenge of developing a strong assurance case for learning-enabled cyber-physical systems (LE-CPS). The starting point for this effort is our prior work, including work in the DARPA High-Assurance Cyber Military Systems (HACMS) program, on hybrid systems modeling and verification utilizing differential dynamic logic (dL). By modeling and verifying LE-CPS in dL, we will provide high-fidelity safety guarantees without relying on discretization, linearization or related simplifications that impact the applicability of safety proofs. Working with UCSD on their Delta-Complete Solving framework we will scale the automatic verification of LE-CPS properties to, e.g., neural networks with on the order of 10000 neurons.

Our dL-Constrained Policy Optimization (dL-CPO) based reinforcement learning will provide a principled approach to safe (online) learning for control and planning subsystems. We will work with CMU to synthesize verified safety monitor conditions with their ModelPlex method. Together with UIUC and RV, we will ensure that these conditions can be used by their RV-Monitor based runtime monitoring infrastructure to produce monitors and guards with low 5-10% runtime overhead without sacrificing safety. Using our Safe Distance approach – quantifying the system's distance from verified safety boundaries – we will evaluate dynamic assurance cases to provide meaningful answers to the question, "How safe is the system?" Our new Expressive Assurance Case Toolkit (ExACT) will provide convenient software interfaces to these innovations. Building on our experience, in applying formal methods techniques and tools to real world platforms, we will apply ExACT to complex real-world LE-CPS and challenge problems. For example, to establishing assurance cases related to collision avoidance by an autonomous car in a range of dynamic and unpredictable scenarios.

This work is funded by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092 for $9,961,662; May 1, 2018 – May 1, 2022. The views, opinions and/or findings expressed are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

High Assurance Cyber Military Systems (HACMS)

As part of the DARPA HACMS program, we developed, integrated, and tested tools and techniques for creating high-assurance software for ground vehicles. In particular, we have integrated, tested, and demonstrated in 2015 a HACMS-based high-assurance controller connected to a 2013 model year American-built passenger automobile, where the HACMS software was controlling acceleration and breaking to achieve both the cruise control capability and the capability to safely stop in front of an obstacle, even when under attack. Later, HRL led the HACMS Ground Integration effort, where HRL is combining a large subset of all HACMS technologies to develop mixed-assurance software toolchain (MAST) and use it to create high-assurance code for two autonomous ground vehicles. Now we are participating in a follow-on effort where we are using similar technologies to develop a high-assurance firewall / domain guard for SCADA type system.

This work is funded by DARPA under AFRL contract FA8750-12-C-0281 for $7,448,761; August 2012 - May 2017 and also by DARPA under AFRL contract FA8750-17C-0035, subcontract PO 4506234540 to Rockwell Collins, April 2017 - June 2018.

Cloud Control Operations Plane (CloudCOP)

CloudCOP is a framework for a secure resilient self-healing cloud. The core of the CloudCOP technology is based on a thin layer of cloud control functionality that is implemented using proactively secure multi-party computation, which we are able to scale to 128 nodes and beyond. The CloudCOP technology establishes a reliable “root-of-trust” built from unreliable nodes, where every node is proactively refreshed from pristine state at regular intervals. It is a fully distributed resilient architecture without any single points of failure that can tolerate ongoing corruption of cloud nodes, within a limit on corruption rate (tunable up to 1/3).

This work was funded by DHS under contract HSHQDC-13-C-B0026 for $3,780,030; September 2013 - April 2018.

Resilient Design and Analysis of Dynamical System Compositions

The traditional approach to the design of complex systems of systems makes extensive use of simulations-e.g., simulating power systems, water supply, and crowd movement-to design for resilience against unexpected or adversarial events. This testing requires extensive sampling of the parameter space to obtain confident predictions on system resilience, limiting the complexity of systems that can be feasibly simulated, and increasing development time and cost. As part of the CASCADE program, we applied theoretical mathematical work from category theory, algebraic topology and operator theory to develop new approaches to system of systems design and analysis that allowed us to cut back on the amount of simulation necessary, while yielding stronger mathematical guarantees on system behavior.

This work was funded by DARPA under SPAWAR contract N66001-16-C-4053 for $971,246; August 2016 - July 2017.

Secure Biometrics

We developed algorithms and software to demonstrate the feasibility of a new provably secure, practical, cryptographic approach that utilizes biometrics to identify and authenticate individuals. Using the fuzzy extractor and fuzzy vault as our main tool, attackers will not have the ability to put the biometric identifiers back together correctly.

Our prototype makes possible secure, leakage-resistant biometrics-based identification, authentication and access control (IAA) systems that do not reveal raw biometric data when data related to the biometrics are obtained from multiple systems.

This work was funded by IARPA under contract 2016-16081000009; September 2016 – September 2017

Tunable Information Flow (TIF)

We had developed a tool and technique for flexible policy-driven software analysis and validation for dynamic environments. Our LLVM-based TIF software analysis tool is capable of statically analyzing software for potential violations of a desired information flow policy, and then instrumenting the software with additional run-time policy checks. This hybrid approach allows us to have a low rate of false positives, while also having a low run-time overhead.

This material is based on research sponsored by the Department of Homeland Security (DHS) Science and Technology Directorate, Cyber Security Division (DHS S&T/CSD), BAA 11-02 and Air Force Research Laboratory Information Directorate via contract number FA8750-12-C-0236 for $2,821,754, September 2012 - March 2016.


Byron Heersink

Gavin Holland

Hyun (Tiffany) Kim

Alexei Kopylov

Joshua Lampkins

Aleksey Nogin

Christopher Serrano

Michael Warren


Click to show/hide the list of Papers

Authors Title Publication Year
William Mansky, Andrew W Appel, Aleksey Nogin A Verified Messaging System Proceedings of the ACM on Programming Languages, Volume 1 Issue OOPSLA. DOI: 10.1145/3133911 2017
Chongwon Cho, Dana Dachman-Soled, Stanisław Jarecki Efficient Concurrent Covert Computation of String Equality and Set Intersection RSA Conference on Topics in Cryptology – (CT-RSA 2016). DOI: 10.1007/978-3-319-29485-8_10 2016
Shlomi Dolev, Karim ElDefrawy, Joshua Lampkins, Rafail Ostrovsky, Moti Yung Proactive Secret Sharing with a Dishonest Majority 10th Conference Security and Cryptography in Networks (SCN), 2016. DOI: 10.1007/978-3-319-44618-9_28 2016
Shlomi Dolev, Karim ElDefrawy, Joshua Lampkins, Rafail Ostrovsky, Moti Yung Brief Announcement: Proactive Secret Sharing with a Dishonest Majority ACM Symposium on Principles of Distributed Computing (PODC), 2016. DOI: 10.1145/2933057.2933059 2016
Karim ElDefrawy, Tiffany Kim, Pape Sylla Automated Identification of Network Service Dependencies via Transfer Entropy 40th IEEE Computer Society International Conference on Computers, Software and Applications (COMPSAC'16), ADMNET: The 4th IEEE International Workshop on Architecture, Design, Deployment and Management of Networks and Applications, 2016. DOI: 10.1109/COMPSAC.2016.68 2016
Karim ElDefrawy, Tyler Kazcmarek Byzantine Fault Tolerant Software-Defined Network (SDN) Controllers 40th IEEE Computer Society International Conference on Computers, Software and Applications (COMPSAC'16), MidCCI: The 2nd IEEE International Workshop on Middleware for Cyber Security, Cloud Computing and Internetworking, 2016. DOI: 10.1109/COMPSAC.2016.76 2016
Joshua Baron, Karim ElDefrawy, Joshua Lampkins, Rafail Ostrovsky Communication-Optimal Proactive Secret Sharing for Dynamic Groups 13th International Conference on Applied Cryptography and Network Security (ACNS), 2015. DOI: 10.1007/978-3-319-28166-7_2. Eprint: ia.cr/2015/304 2015
Karim ElDefrawy, Gavin Holland, Gene Tsudik (Extended Abstract) Remote Attestation of Heterogeneous Cyber-Physical Systems: The Automotive Use Case 2015 Embedded Security in Cars USA (escar USA) Workshop 2015
Karim ElDefrawy, Joshua Lampkins Founding Digital Currency on Secure Computation 2014 ACM Conference on Computer and Communications Security (CCS'14). DOI: 10.1145/2660267.2660293 2014
Karim ElDefrawy, Joshua Lampkins Disincentivizing/Incentivizing Malicious/Honest Behavior on the Internet Via Privacy-preserving AppCoins 2014 Workshop on Secure Network Protocols (NPSec'14). DOI: 10.1109/ICNP.2014.100 2013
Joshua Baron, Karim ElDefrawy, Joshua Lampkins, Rafail Ostrovsky How to Withstand Mobile Virus Attacks, Revisited 2014 ACM Principles of Distributed Computing (PODC'14). DOI: 10.1145/2611462.2611474. Eprint: ia.cr/2013/529 2012
Chongwon Cho, Sanjam Garg, Rafail Ostrovsky Cross-Domain Secure Computation 2014 International Conference on Public-Key Cryptography (PKC’14). DOI: 10.1007/978-3-642-54631-0_37 2014
Joshua Baron, Karim ElDefrawy, Aleksey Nogin, Rafail Ostrovsky An Architecture for Resilient Cloud Operations IEEE International Conference on Technologies for Homeland Security (HST) 2013. DOI: 10.1109/THS.2013.6699036 2013
Joshua Baron, Karim ElDefrawy, Kirill Minkovich, Rafail Ostrovsky, Eric Tressler “5PM: Secure Pattern Matching,”, the SCN'12 special issue of Journal of Computer Security 8th conference on Security and Cryptography for Networks (SCN) 2012. DOI: 10.1007/978-3-642-32928-9_13 Eprint: ia.cr/2012/698. 2013
Karim ElDefrawy, Sky Faber Blindfolded Searching of Data via Secure Pattern Matching IEEE Computer Magazine’s Special Issue on Cyber Security December 2013. DOI: 10.1109/MC.2013.73 2013
Karim ElDefrawy, Gavin Holland Secure and Privcay-preserving Querying of Content in MANETs IEEE International Conference on Technologies for Homeland Security (HST) 2012. DOI: 10.1109/THS.2012.6459917 2012
Karim ElDefrawy, Aurelien Francillon, Daniele Perito, Gene Tsudik SMART: Secure and Minimal Architecture for (Establishing Dynamic) Root of Trust Network and Distributed System Security Symposium (NDSS) 2012 2012

Click to show/hide the list of Patents

Authors Title Patent # Date
Aleksey Nogin, Kirill Minkovich, Karim El Defrawy, Joshua W Baron, Eric P Tressler, Gavin D Holland System and method for cloud control operations plane based on proactive security algorithms US 9,846,596 December 19, 2017
Gavin D. Holland, David L. Allen Self-healing array system and method US 9,702,928 July 7, 2017
David L. Allen, Gavin D. Holland Antenna array optimization system US 9,553,363 January 24, 2017
Karim El Defrawy, Joshua D. Lampkins Method for secure and resilient distributed generation of elliptic curve digital signature algorithm (ECDSA) based digital signatures with proactive security US 9,467,451 November 8, 2016
Joshua W. Baron, Karim El Defrawy, Joshua D. Lampkins Generic proactively-secure secret-sharing protocol from any suitable honest-majority secret-sharing protocol US 9,467,451 October 11, 2016
Joshua D. Lampkins, Karim El Defrawy, Joshua W. Baron Information secure proactive multiparty computation (PMPC) protocol with linear bandwidth complexity US 9,450,938 September 20, 2016
Karim El Defrawy, Joshua W. Baron General protocol for proactively secure computation US 9,449,177 September 20, 2016
Karim El Defrawy, Joshua D. Lampkins System and method for mobile proactive secret sharing US 9,443,089 September 13, 2016
George Kuan, Aleksey Nogin, Alexei Kopylov System for information flow security inference through program slicing US 9,378,377 June 28, 2016
Heiko Hoffmann, Michael J. Daily, Gavin D. Holland, Karim El Defrawy System and method for deep packet inspection and intrusion detection US 9,336,239 May 10, 2016
Alexei Kopylov, George Kuan, Aleksey Nogin Library-based method for information flow integrity enforcement and robust information flow policy development US 9,317,682 April 19, 2016
Tsai-Ching Lu, Hankyu Moon, Gavin D. Holland, David L. Allen, Aleksey Nogin, Michael D. Howard System and methods for digital artifact genetic modeling and forensic analysis US 9,224,067 December 29, 2015
Aleksey Nogin System and method for asynchronous explanation and propagation-based constraint solving US 9,147,160 September 29, 2015
Gavin D. Holland, Karim M. El Defrawy Wireless network security US 9,119,077 August 25, 2015
Aleksey Nogin, Joshua Baron, Karim El Defrawy System for ensuring that promises are kept in an anonymous system US 9,026,786 May 5, 2015
Hankyu Moon, Tsai-Ching Lu System for Instability Detection and Structure Estimation of Complex Network Dynamics US 9,368,804 March 24, 2015
Karim El Defrawy, Kirill Minkovich, Joshua W. Baron, Eric P. Tressler, Heiko Hoffmann Secure pattern matching US 9,009,089 April 14, 2015
Aleksey Nogin, Yang Chen Revision control server with self-hosting multi-level access controls and user notifications US 8,990,249 March 24, 2015
Shengbing Jiang, Aleksey Nogin Efficient source of infeasibility identification in timed automata traces US 8,645,310 February 4, 2014
Gavin D. Holland, Karim M. El Defrawy Wireless network security US 8,612,743 December 17, 2013
Gavin D Holland, Fan Bai, Hariharan Krishnan Systems and methods for multi-channel medium access control US 8,400,987 March 19, 2013
David W. Payton, Aleksey Nogin Establishing common interest negotiation links between consumers and suppliers to facilitate solving a resource allocation problem US 8,370,422 February 5, 2013


Press Releases

|Hacking Back at the Hackers
|The ExACT Tools for Safe Autonomy

Media Coverage

08/01/2017 | HRL Horizons features CSRS


Past Events

December 14-15, 2016

1st International seL4 Workshop; Co-organized with CSIRO Data 61 team

Current Openings for CSRS

|Summer Internship in AI Security
|Scientist IV – Assured Autonomy
|Scientist IV – Formal Verification & Synthesis
|Scientist IV – Post Doctorate: Formal Verification & Synthesis


Email: anogin[at]hrl.com

Dr. Aleksey Nogin
Senior Research Staff Computer Scientist
Leader, Center for Secure and Resilient Systems

Information and Systems Sciences Lab
HRL Laboratories, LLC
3011 Malibu Canyon Road
Malibu, CA 90265