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.
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
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.
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.
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.
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.
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.
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.
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.
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
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.
|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|
|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|
December 14-15, 2016
1st International seL4 Workshop; Co-organized with CSIRO Data 61 team
||||Scientist IV – Post Doctorate: Formal Verification & Synthesis|
||||Scientist IV – Formal Verification & Synthesis|
||||Scientist IV – Assured Autonomy|
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