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.

Research

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.

People


Byron Heersink


Gavin Holland


Hyun (Tiffany) Kim


Alexei Kopylov


Joshua Lampkins


Aleksey Nogin


Shane Roach


Christopher Serrano


Pape Sylla


Michael Warren

Publications

Click to show/hide the list of Papers

Authors Title Publication Year
Christopher Serrano, Pape Sylla, Sicun Gao, Michael Warren RTA3: A Real Time Adversarial Attacks on Recurrent Neural Networks Deep Learning Security 2020, IEEE Security & Privacy Workshops 2020
Tiffany Hyun-Jin Kim, Joshua Lampkins SSP: Self-Sovereign Privacy for Internet of Things Using Blockchain and MPC Proceedings of the 2019 IEEE International Conference on Blockchain. DOI: 10.1109/Blockchain.2019.00063 2019
Christopher Serrano, Michael Warren Introspection Learning AAAI Spring Symposium on Verification of Neural Networks (VNN19) 2019
Tiffany Hyun-Jin Kim, Joshua Lampkins BRICS: Blockchain-based Resilient Information Control System Proceedings of the 2018 IEEE International Conference on Big Data. DOI: 10.1109/BigData.2018.8621993 2018
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
Hyun J Kim, Chong Ding, Karim El Defrawy Systems and methods for generating filtering rules US 10,530,696 January 7, 2020
Chongwon Cho, Karim El Defrawy, Hyun (Tiffany) Kim, Joshua Lampkins Privacy-preserving multi-client and cloud computation with application to secure navigation US 10,528,760 January 7, 2020
Karim El Defrawy, Joshua W. Baron System and method to integrate secure and privacy-preserving biometrics with identification, authentication, and online credential systems US 10,523,654 December 31, 2019
Chongwon Cho, Karim El Defrawy One-time obfuscation for polynomial-size ordered binary decision diagrams (POBDDs) US 10,509,918 December 17, 2019
George Kuan, Aleksey Nogin System and method for maintaining security tags and reference counts for objects in computer memory US 10,430,587 October 1, 2019
Karim El Defrawy, Ian A. Maxon, Matthew S. Keegan, Tsai-Ching Lu Inferring network services and their dependencies from header and flow data and the switching topology US 10,425,489 September 24, 2019
Karim El Defrawy, Joshua D. Lampkins System and method for operating a proactive digital currency ledger US 10,423,961 September 24, 2019
Alexei Kopylov, Aleksey Nogin System and method for synthesis of correct-by-construction cryptographic software from specification US 10,423,780 September 24, 2019
Alexei Kopylov, Aleksey Nogin, George Kuan System and method for translating security objectives of computer software to properties of software code US 10,402,584 September 3, 2019
George Kuan, Aleksey Nogin, Alexei Kopylov Language-based missing function call detection US 10,366,232 July 30, 2019
Karim El Defrawy, Joshua W. Baron Protocol for securely searching streaming data with constant bandwidth US 10,346,617 July 9, 2019
Karim El Defrawy, Michael J. O'Brien, James Benvenuto Lattice-based inference of network services and their dependencies from header and flow data US 10,243,811 March 26, 2019
Pape Sylla, Hyun Jin Kim, Karim El Defrawy Mapping network service dependencies US 10,200,482 February 5, 2019
Karim El Defrawy, Chongwon Cho, Daniel C. Apon, Jonathan Katz Non-malleable obfuscator for sparse functions US 10,198,584 February 5, 2019
Karim El Defrawy, Gavin D. Holland Method and apparatus for secure and privacy-preserving querying and interest announcement in content push and pull protocols US 10,181,049 January 15, 2019
Karim M. El Defrawy, Pape M. Sylla Firewall filter rules generation US 10,158,606 December 18, 2018
Karim El Defrawy, Hyun Jin Kim, Pape Maguette Sylla, Ryan F. Compton Mapping network service dependencies US 10,129,342 November 13, 2018
Gavin Holland, Michael Howard, Chong Ding System and method to detect attacks on mobile wireless networks based on network controllability analysis US 10,091,218 October 2, 2018
Aleksey Nogin, George Kuan, Alexei Kopylov System for detecting source code security flaws through analysis of code history US 10,084,819 September 25, 2018
Joshua D. Lampkins, Karim El Defrawy System and method for mobile proactive secure multi-party computation (MPMPC) using commitments US 10,083,310 September 25, 2018
Gavin Holland, Michael Howard, Tsai-Ching Lu, Karim El Defrawy, Matthew S. Keegan, Kang-Yu Ni System and method for determining reliability of nodes in mobile wireless network US 10,003,985 June 19, 2018
Gavin Holland, Michael Howard, Chong Ding, Tsai-Ching Lu System and method to detect attacks on mobile wireless networks based on motif analysis US 9,979,738 May 22, 2018
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
Joshua D. Lampkins, Karim El Defrawy Information secure protocol for mobile proactive secret sharing with near-optimal resilience US 9,787,472 October 10, 2017
Gavin D. Holland, David L. Allen Self-healing array system and method US 9,702,928 July 7, 2017
Karim El Defrawy, Pape Maguette Sylla Mapping network service dependencies US 9,628,553 April 18, 2017
Karim El Defrawy, Joshua D. Lampkins, Joshua W. Baron Cryptographically-secure packed proactive secret sharing (PPSS) protocol US 9,614,676 April 4, 2017
Karim El Defrawy, Kirill Minkovich, Joshua W. Baron, Eric P. Tressler Secure multi-dimensional pattern matching for secure search and recognition US 9,613,292 April 4, 2017
Karim El Defrawy, Joshua W. Baron, Joshua D. Lampkins Information theoretically secure protocol for mobile proactive secret sharing with near-optimal resilience US 9,558,359 January 31, 2017
David L. Allen, Gavin D. Holland Antenna array optimization system US 9,553,363 January 24, 2017
Karim El Defrawy, Joshua D. Lampkins Secure mobile proactive multiparty computation protocol US 9,536,114 January 3, 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
David L. Allen, Tsai-Ching Lu, Eric P. Tressler, Hankyu Moon System and method for insider threat detection US 9,043,905 May 26, 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

News

Press Releases

11/16/2018
|Hacking Back at the Hackers
05/03/2018
|The ExACT Tools for Safe Autonomy

Media Coverage

08/01/2017 | HRL Horizons features CSRS

Events

Past Events

December 14-15, 2016

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

Current Openings for CSRS

141
|Scientist V – Assured Autonomy
63
|Scientist IV – Assured Autonomy
65
|Scientist IV – Formal Verification & Synthesis

Contact

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
USA