2024 Summit

Current Technology Advances and Modern Software Development

Fifth Annual Summit Technical Program

May 9-10, 2024 | Annapolis, MD, USA
This year, the TCCOE Summit will be held jointly again with the 2024 High Confidence Software and Systems Conference (HCSS) during May 6-8 at the same venue. The Trusted Computing Center of Excellence has been established with support from DARPA, AFRL, and Griffiss Institute. The TCCOE seeks to support the Department of Defense’s (DoD) National Security mission through the transition and insertion of trustworthy software into the systems employed by the DoD to execute that mission. The TCCOE recognizes that the DoD incurs risk upon the execution of software, to minimize that risk there needs to be evidence supporting the trustworthiness of the software. Rigorous mathematical verification can offer the strongest evidence of trustworthiness but heretofore has faced numerous impediments to practical use. The TCCOE recognizes that we are at a technological inflection point in the maturation and capability to perform such verifications. The TCCOE will champion the insertion of trustworthy software into defense systems in a sound and prudent fashion. This year, the main theme of the TCCOE Summit is ‘Current Technology Advances and Modern Software Development’. Similar to previous years, the Summit will include technical talks and expert panels on various tools and techniques.
view previous summit topics
registration
agenda
Thursday, May 9, 2024 Current Technology Advances and Modern Software Development
Chair & Time Introduction and Keynote Dr. Jason LiDr. Sergey Bratus, Dartmouth University 08:45 AM – 09:45 AM Presentation Break (15 minutes) 09:45 AM - 10:00 AM
  • TrustZone-Based Attestation Framework for Untrusted Operating Environments Patrick Hurley
  • Tom Barnett (DEVCOM/AvMC)/Zachary Clark (DornerWorks) 10:00 AM – 10:30 AM
  • Presentation
  • Computers don’t go to high school, or: Safety and Security Risks Induced by Computer Arithmetic
  • Thomas Wahl, GrammaTech 10:30 AM - 11:00 AM
  • Presentation
  • seL4 Ecosystem update
  • Gernot Heiser & June Andronick, seL4 Foundation 11:00 AM - 11:30 AM
  • Presentation
  • A Policy-free Kernel for Scalable Multi-core, Bounded Execution, and Verification
  • Gabriel Parmer, George Washington University 11:30 AM - 12:00 PM
  • Presentation
  • Lunch 12:00 PM - 01:30 PM
  • The Benefits of Performing Comprehensive Memory Safety Validation Trent Jaeger, UC Riverside 01:30 PM - 02:00 PM
  • Presentation
  • Leveraging Rust in seL4 user space
  • Nick Spinale, Colias Group, LLC 02:00 PM - 02:30 PM
  • Presentation
  • Building Security and Resilience on ARM Morello Systems
  • Eric Hwang, Trusted Science and Technology 02:30 PM - 03:00 PM
  • Presentation
  • Building Dependable Embedded Systems with Open-Source Components
  • Kate Stewart, VP Dependable Embedded Systems, The Linux Foundation 03:00 PM - 03:30 PM
  • Presentation
  • Break (30 minutes) 03:30 PM - 04:00 PM
  • Panel Discussion – Technology Advances and Modern Software Development
  • Moderator: Ray Richards 04:00 PM - 05:00 PM
  • Dr. Sergey Bratus, Dartmouth University
  • Dr. Trent Jaeger, UC Riverside
  • Ms. Kate Stewart, The Linux Foundation
  • Dr. Ryan Craven, ONR
  • END OF DAY ONE
Friday, May 10, 2024 Current Technology Advances and Modern Software Development
Chair & Time Introduction and Keynote Dr. Jason LiDr. Ryan Craven, ONR 08:45 AM – 09:45 AM Presentation Break (15 minutes) 09:45 AM - 10:00 AM
  • Expanding AADL Code Generation and Formal Methods Tooling to SysMLv2 Patrick Hurley
  • Dr. John Hatcliff, Kansas State University 10:00 AM – 10:30 AM
  • Presentation
  • Enabling Lightweight Secure Containers,
  • Hui Lu, University of Texas at Arlington 10:30 AM - 11:00 AM
  • Presentation
  • High Assurance Containerization for Multi-Level Security in the Cloud
  • Dr. Nathan Daughety, AFRL/RIGA 11:00 AM - 11:30 AM
  • Presentation
  • Learning Environments for Developing Autonomous Cyber Agents
  • Dr. Daniel Balasubramanian, Vanderbilt University 11:30 AM - 12:00 PM
  • Presentation
  • Updates from TCCOE
  • Patrick Hurley, TCCOE 12:00 PM - 12:15 PM
  • Presentation
  • Closing Remarks
  • Brad Martin, DARPA
  • Dr. Nathan Daughety, Air Force Research Laboratory 12:15 PM - 12:30 PM

END OF DAY TWO

Meet the Speakers

The Benefits of Performing Comprehensive Memory Safety Validation

Trent Jaeger, UC Riverside
Trent Jaeger is a professor in the Computer Science and Engineering Department at the University of California, Riverside, after 18 years at Penn State University. His research interests include systems and software security, having made many contributions to the Linux open-source community. He has served as Chair of the ACM Special Interest Group on Security, Audit, and Control (ACM SIGSAC) and as the Steering Committee Chair for the Internet Society Network and Distributed Systems Symposium (NDSS). He is currently an Associate Editor-in-Chief for IEEE Security & Privacy and on the Editorial Board for the Communications of the ACM.
Researchers have rightfully been concerned about preventing memory errors, but have ignored methods to improve the security of the parts of the program that are already memory-safe. We propose techniques to perform comprehensive memory safety validation that identify the program objects whose accesses probably comply with all classes of memory safety. We have found that a large fraction of program objects only have aliases (computed conservatively) satisfy memory safety comprehensively whose accesses all satisfy memory safety comprehensively and that these fractions are increasing. Our results show that over 85% of stack objects and over 75% of heap objects in over 1,200 Linux Ubuntu packages can comprehensively be validated as satisfying memory safety. We discuss some immediate benefits that can be realized by leveraging these results, such as low overhead protection from memory errors, as well as some opportunities to explore in the future. Finally, we discuss research directions to utilize the knowledge learned from comprehensive memory safety validation to prevent memory errors in access to the remaining, unsafe objects.

sysMesh: System Service Mesh to Secure Container‑based Orchestration Platforms

Hui Lu
Dr. Hui Lu is an Assistant Professor at the University of Texas at Arlington, previously at SUNY Binghamton. His research covers operating systems, virtualization, cloud computing, and network systems. He has collaborated with top labs like HPE, IBM, Microsoft, AT&T, and NEC, and holds a Ph.D. from Purdue University. Prior to his doctorate, he was a performance engineer at Intel's Asia-Pacific R&D Center and earned his bachelor's and master's degrees from Shanghai Jiao Tong University.
One key force that drives today’s cloud revolution is the adoption of microservices architecture – an architectural style that transforms monolithic applications into graphs of smaller, simpler, and loosely coupled components, namely microservices. Microservices are further containerized and managed through cloud orchestration platforms like Borg, Apache Mesos, Kubernetes, and Docker Swarm. These orchestration platforms play a central role in 1) handling the management nuances of containers, networking, scalability, load balancing, and logging, 2) removing the burden of repetitive manual processes in container management, and 3) speeding up the service deployment process. While orchestration platforms transform the way one builds, deploys, and manages modern applications, it results in critical security threats and concerns as the code base and attack surface of such platforms increase. Security issues involve multiple layers ranging from containers to orchestrators, networking, and additional services like service mesh or custom operators. As these orchestration platforms continue to develop, new vulnerabilities will inevitably emerge, potentially affecting any of the components involved in orchestration. While there is no single bullet to tackle these threats effectively, implementing security measures for a thorough understanding and timely detection/prevention of vulnerabilities in orchestration platforms is essential. We propose sysMesh, an innovative security framework designed to offer a layered security approach through the integration of system sidecars into key components of orchestration components. With sysMesh, various security measures and features can be readily realized, hence significantly increasing the security and assurance of container‑based orchestration environments. The project will generate building‑block approaches in enabling secured orchestration platforms, including a foundational sysMesh framework, various sysMesh sidecars for distinct security features, and exposing new vulnerabilities.

Secure Boot Hardware-Software Attestation of Networked Systems

Tom Barnett, DEVCOM/AvMC Zachary Clark, DornerWorks
Mr. Clark- Embedded software engineer with a specific focus in embedded virtualization and securely networked systems. Obtained undergraduate degree in electrical and computer engineering from Calvin University. Studies contained an emphasis on computer science and software engineering, and design projects focused on ensuring system safety and security within the wider context of software development.
As the connectivity of systems increases, the attack surface of connected systems also increases. Trusted computing requires that only legitimate software be run on target platforms to help minimize security risks. Secure Boot can be utilized to ensure the integrity of software images at boot time, though for networked platforms, this can be further improved upon through attestation. However, a compromised system may also have its attestation software compromised. This talk will cover an Arm TrustZone-based architecture for performing attestation for networked systems, all while being isolated from the rest of a virtualized system. This architecture provides product developers with the ability to introspect and attest many aspects of their system, including the hypervisor, while operating in a hardware-enforced isolated environment, thus mitigating many exploits commonly seen when using purely software-based isolation.

seL4 Ecosystem update

Gernot Heiser June Andronick
Mr. Heiser- Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney. His research interests are in operating systems, real-time systems, security, and safety. His research vision is to completely change the cybersecurity game from playing catch-up with attackers to provably secure systems. As a leader of the Trustworthy Systems group, he pioneered large-scale formal verification of systems code, specifically the design, implementation, and formal verification of the seL4 microkernel; seL4 is now being used in real-world security- and safety-critical systems. Ms. Andronick- June Andronick is the CEO and co-founder of Proofcraft, a company conducting verification projects and providing commercial support, training, or consulting on formal verification in general and involving the seL4 microkernel specifically. June has extensive leadership experience in making the vision of verified software a reality in mainstream critical software. She was previously leading the Trustworthy Systems group, and contributed to the original seL4 verification. She is a Conjoint Professor at UNSW Sydney, Australia. June is also CEO of the seL4 Foundation.
The talk will give an update on what happened in the seL4 Foundation over the past year or so. Specific highlights include the successful seL4 Summit in Minneapolis. Technical highlights include the adoption of the seL4 Microkit, which dramatically reduces the barrier to uptake for seL4 and the official support for developing seL4-based applications in Rust. We will also cover work in progress on various open-source building blocks. Highlights here are:- progress on the verification of the 64-bit Arm version of seL4 (should be completed by the time of the talk)- progress on verification of the MCS variant and the multicore version of seL4- automated verification of the Microkit- development tool support (debugging, profiling)- device driver framework that simplifies driver development and supports high-performance I/O- development of a complete, open-source reference system (a point-of-sale system)

A Policy-free Kernel for Scalable Multi-core, Bounded Execution, and Verification

Gabriel Parmer
Gabriel Parmer (https://faculty.cs.gwu.edu/gparmer/) is the head of the embedded systems and Operating Systems groups at GWU. Core contributions of these groups are in the Composite, component-based microkernel, and in omnipresent webassembly runtimes, the papers for which have received five paper awards.
Microkernels have long aimed to have policy-free kernels, thus enabling competing, user-level policies. This goal has been quite difficult to realize completely, and popular microkernels make practical trade-offs between policy freedom and performance. In this talk, we'll discuss many of the challenges that afflict systems that cannot extricate policy from the kernel and the benefits that the Composite microkernel has from its insistent focus on policy freedom. These benefits include scalable multi-core execution, and real-time predictability due to bounded execution and timing, and we'll share some initial results on automatic functional verification.

Leveraging Rust in seL4 userspace

Nick Spinale Colias Group, LLC
Nick Spinale is an independent computer security researcher and consultant based in Portland, Oregon. He specializes in developing and applying techniques for constructing trustworthy system software. Before forming his consultancy, he was a member of Arm Research in Cambridge, UK.
The Rust programming language and ecosystem provide memory safety and enhance developer productivity even at lower levels of the software stack. As evidenced by recent relevant milestones including the qualification of a Rust toolchain for use in safety-critical environments and the language’s inclusion in the Linux kernel, Rust is ready for this community’s applications. This talk outlines our efforts, funded by the seL4 Foundation, to apply Rust to the seL4 userspace and facilitate its use in the seL4 software ecosystem. Furthermore, this talk also demonstrates what this progress means for teams developing and delivering seL4-based systems.

Building Dependable Embedded Systems with Open Source Components

Kate Stewart VP Dependable Embedded Systems The Linux Foundation
Kate works with the safety, security and license compliance communities to advance the adoption of best practices into embedded open source projects. Since joining The Linux Foundation, she has launched the ELISA and Zephyr Projects, as well as supporting other embedded projects. With more than 30 years of experience in the software industry, she has held a variety of roles in software development, architecture, and product management, primarily in the embedded ecosystem. She has presented on SBOMs, embedded systems and more, at industry conferences like RSA Conference, IoT World, Embedded World, Open Source Summit among others.
Systems are no longer created from monolithic code bases, they are composed of components that are integrated over time, and maintained by different entities. Yet for a system to be dependable, they all need to be integrated together and tested as updates occur to demonstrate they still adhere to the necessary requirements. Open Source projects are increasingly being used as the components in these systems. Effective system engineering depends on requirements being tested for the system as a whole and for the components, however, open-source projects frequently don't have requirements expressed in a form that is consumable. This talk will look at a proposed framework for a system bill of materials that will enable those components providing requirements to be integrated so that product lines can be managed, and those open source components able to surface up their requirements can be integrated.

Learning Environments for Developing Autonomous Cyber Agents

Dr. Daniel Balasubramanian
Dr. Daniel Balasubramanian is a Senior Research Scientist at the Institute for Software Integrated Systems and an Adjunct Associate Professor in the School of Engineering at Vanderbilt University. He is currently a PI on the DARPA Cyber Agents for Security Testing and Learning Environments (CASTLE) program, the DARPA Verified Security and Performance Enhancement of Large Legacy Software (V-SPELLS) program, and the DARPA Business Process Logic (BPL) program, a co-PI on the DARPA Space-Time Analysis for Cybersecurity (STAC) program, was the PI on an NSF Smart and Connected Communities project.
Modern software systems rely not only on testing and verification techniques to ensure their correctness and availability but also on a variety of runtime defenses. As attack surfaces have spread across multiple layers of the computing stack, from the hardware to the OS, to libraries, to the application, defending against sophisticated attacks spanning multiple layers has become an even greater challenge. Autonomous cyber agents offer the promise of automating the defense against such complex attacks, but developing agents capable of reasoning across multiple layers of the computing stack is a challenging task. This talk will present our preliminary work on developing a reinforcement learning environment in which autonomous agents can be trained to defend against these types of attacks that are spread across multiple layers of the computing stack. Central to our work is the idea of an “operational workflow”, which defines the critical nodes and services that an agent must learn to maintain in the presence of an attack.

Building Security and Resilience on ARM Morello Systems

Eric Hwang Jason Li
CHERI (Capability Hardware Enhanced RISC Instructions) extends processor Instruction Set Architectures (ISAs) with architectural capabilities to enable fine-grained memory protection. The most significant effort is Arm Morello, an adventure launched by Arm and the UK government to develop an industrial demonstrator of a capability architecture. Trusted Science and Technology (Trusted ST) is working with the United States Defense Advanced Research Projects Agency (DARPA) to evaluate the benefits of CHERI technologies and feasible software stack to enhance system security and resilience on top of ARM-Morello platforms. This effort contains two development and evaluation paths: (1) The microkernel path leverages previous seL4-based security and resilience solutions, making the kernel CHERI-aware without requiring CHERI capability enforcement in the kernel; and (2) The CheriBSD path delivers a similar level of security and resilience without relying on a separation kernel. Trusted ST has made significant progress along both of these development paths. In this presentation, we will showcase our journey and lessons learned.

"Computers don't go to high school, or: Safety and Security Risks Induced by Machine Arithmetic "

Thomas Wahl
Thomas Wahl is a Principal Researcher at GrammaTech, Inc., which he joined in 2021, after an extended career in academia. Thomas served as a faculty member at Northeastern University in Boston in 2011. He obtained a PhD in Computer Science from the University of Texas at Austin in 2007.
Thomas' general research interest is the automated analysis of software using mathematically rigorous model-theoretic or proof-theoretic techniques (AKA Formal Methods), to identify critical program errors or vulnerabilities. His special expertise lies in the analysis of concurrent and numeric programs. He has worked on the detection of information leaks introduced by compilers, and of structural and quantitative manipulations on neural networks to influence their decision-making.
Floating-point arithmetic (FPA), the most widely used approximation of real arithmetic on computers, often delivers inaccurate and occasionally outright algebra-defying numeric results. This restrains optimizing compilers and confuses humans and their high school memories, but we mostly live with that. Less known is that FPA implementations are by design only loosely standardized, which makes numeric computations architecture-dependent and thus hard to reproduce, potentially causing surprising cross-platform code behaviors. Worse, special values in FPA allow attackers to reverse-engineer otherwise secret information about the source code or the involved data.In this talk I will first give some brief background on FPA, its design decisions, fundamental consequences of these decisions, and alternatives to FPA and why we do or do not use them. I will discuss existing floating-point standards and why even compliant FPA implementations are not guaranteed to agree on the results from numeric computations. I will then illustrate the problems sketched in the previous paragraph: We will see how programs compiled for specific platforms can give rise to entirely botched calculations, how control flow can make wrong turns due to aggressive code optimizations, and how IP in neural networks can be stolen simply by exploiting quirks of FPA. Time permitting, I will sketch what technology is available to investigate floating point-induced reliability and security problems.

Expanding AADL Code Generation and Formal Methods Tooling to SysMLv2

Dr. John Hatcliff Kansas State University
Dr. John Hatcliff is a University Distinguished Professor and Lucas-Rathbone Professor of Engineering at Kansas State University working in the areas of safety-critical systems, software architectures, and software verification and certification. He leads the Laboratory on Specification, Analysis, and Transformation of Software (SAnToS Lab), whose research has been funded by national funding agencies and companies including Department of Defense, National Science Foundation, DARPA, Department of Homeland Security, US Army, NASA, NIH, ARO, Air Force Office of Scientific Research, SEI, Collins Aerospace, Galois, and Lockheed Martin.
In this talk, I will describe how we have shown it is technically feasible to drive several AADL-based high-assurance development technologies from SysMLv2. I'll first describe how we have extended the HAMR model-driven development code generation framework to support a subset of SysMLv2. HAMR provides code generation capabilities for the verified seL4 micro-kernel, as well as Linux and the JVM. HAMR was a key component of the Collins Aerospace DARPA CASE tool suite, and it will play a similar role in the upcoming Collins DARPA PROVERS project. I'll illustrate the framework with example system SysMLv2 models and generated code for seL4. I'll also give an overview of how the GUMBO component contract language, jointly developed with Galois engineers, as well as SMT-based verification and automated property-based randomized testing technologies, will be supported in the toolchain. I'll discuss how HAMR's code generation capabilities will be expanded on DARPA PROVERS to include Rust code generation and support for seL4 Microkit (Core Platform) (as a replacement for the CAmkES framework). The talk will conclude with broader perspectives about the need for a SysMLv2-based model-driven development toolchain to support high-assurance application development for kernel-based platforms, including those enabled by seL4.HAMR is available under an open-source license, and the project website includes an example repository and collection of videos, tutorials, and classroom lecture materials (also suited for workforce training).

High Assurance Containerization for Multi-Level Security in the Cloud

Dr. Nathan Daughety AFRL/RIGA
Nathan Daughety is a research scientist at the Air Force Research Laboratory. He earned his Doctorate from the University of Cincinnati in Computer Science and Engineering with a focus in Cyber Operations. The presented work is in the area of secure containerization which follows from previous publications and a patent for a cross-domain solution architecture.
Containerization has overtaken virtualization in software deployment technology in production environments and has been a catalyst for DevSecOps workflows and CI/CD pipelines. Moreover, containers can provide a tremendous advantage to DoD technologies like cross-domain solutions (CDS) with the operational shift to the cloud and the need to rapidly deploy capabilities and adjust to dynamic operational priorities. However, containerization introduces critical risks to the warfighting mission. Specifically, containers were not designed to provide a strong security boundary and do not effectively provide the following security properties: Data Separation, Authorized Information Flow, Assured Sanitization, Damage Limitation, and Attestation. Furthermore, substantial security gaps exist around the Ops portion of DevSecOps, with an emphasis on security in deployment. This work presents research that aims to provide guarantees on container behavior that enforce security requirements of the software and host environments while working within existing technology stacks. A method will be presented in which lightweight containers can be deployed in the cloud, leveraging the formally verified microkernel, seL4. The objective of this work is to develop a high-assurance containerization architecture to be leveraged in critical cross-domain environments.
seL4 is a trademark of LF Projects, LLC. Trusted Computing Center of Excellence™ is a tradename of The Computing Center of Excellence, Inc. Copyright © 2022 The Computing Center of Excellence, Inc.