2025 Summit

Technology Advances, Trust and Trustworthiness, and Software Ecosystems

Seventh Annual Summit Technical Program

May 15-16, 2025 | Annapolis, MD, USA
view previous summit topics
registration
agenda
Thursday, May 15, 2025 Technology Advances, Trust and Trustworthiness, and Software Ecosystems
Chair & Time Introduction and Keynote Dr. Ray RichardsDr. Bill Scherlis, Carnegie Mellon University 08:45 AM – 09:45 AM Presentation Break (15 minutes) 09:45 AM - 10:00 AM
  • MonT: Toward Real-time Model Checking Dr. Stuart Card
  • Dr. Sukarno Mertoguno, Georgia Tech 10:00 AM – 10:30 AM
  • Presentation
  • Secure High-Assurance Aberdeen Architecture RISC-V Complier and Softcore (SHAAARCS)
  • Dr. Michael Doran, DornerWork 10:30 AM - 11:00 AM
  • Presentation
  • Hardware Attacks and Defenses for High Assurance Systems
  • Dr. Sean Zhou, Trusted Science and Technology 11:00 AM - 11:30 AM
  • Presentation
  • Kry10 OS - Trustworthy, Dynamic, and Easy To Us
  • Dr. Ihor Kuz, Kry10 11:30 AM - 12:00 PM
  • Presentation
  • Lunch 12:00 PM - 01:30 PM
  • Patrick Hurley
  • LITESHIELD: A Lightweight Userspace μKernel Architecture for Secure Container Isolation Dr. Hui Lu, University of Texas at Arlington 01:30 PM - 02:00 PM
  • Presentation
  • Unikernels: A DevSecOps alternative to containers
  • Robbie VanVossen, DornerWorks 02:00 PM - 02:30 PM
  • Presentation
  • Mobile Software Understanding for Compound Vulnerabilities Using Knowledge Graph (KG) and Graph Neural Network (GNN)
  • Fei Sun, Leidos 02:30 PM - 03:00 PM
  • Presentation
  • Secure Robotic Operating System (seROS)
  • Nathan Studer, DornerWorks 03:00 PM - 03:30 PM
  • Presentation
  • Break (30 minutes) 03:30 PM - 04:00 PM
  • Panel Discussion – Technology Advances, Trust, and Trustworthines
  • Moderator: Dr. Ray Richards 04:00 PM - 05:00 PM
  • Dr. Evan Austin, Leidos
  • Dr. Trent Jaeger, UC Riverside
  • Dr. Steve Kuhn, DARPA
  • Dr. Sandeep Neema, Vanderbilt University
  • END OF DAY ONE
Friday, May 16, 2025 Technology Advances, Trust and Trustworthiness, and Software Ecosystems
Chair & Time Introduction and Keynote Dr. David MuslinerDr. Trent Jaeger, UC Riverside 08:45 AM – 09:45 AM Presentation Break (15 minutes) 09:45 AM - 10:00 AM
  • Building a Memory Safe Software Ecosystem with CHERI Dr. Jason Li
  • Brooks Davis, SRI 10:00 AM – 10:30 AM
  • Presentation
  • Fine-Grained Security Control through Combined Memory Access Protection and Isolation
  • Dr. Thomas Wahl, Trusted Science and Technology 10:30 AM - 11:00 AM
  • Presentation
  • Exploring Next-Generation Hardware Platforms to Harness the Benefits of CHERI Experimental Implementations
  • Dr. Hui Zeng, PJR Corp 11:00 AM - 11:30 AM
  • Presentation
  • SWITCHing to CHERI – Smoothing the Path to Cyber Security
  • Dr. David Musliner, Smart Information Flow Technologies (SIFT) 11:30 AM - 12:00 PM
  • Presentation
  • Updates from TCCOE
  • Patrick Hurley, TCCOE 12:00 PM - 12:15 PM
  • Presentation
  • Closing Remarks
  • Dr. Ray Richards, Leidos 12:15 PM - 12:30 PM

END OF DAY TWO

Meet the Speakers

MonT: Toward Real-time Model Checking

Dr. Sukarno Mertoguno Georgia Tech
Dr. J. Sukarno Mertoguno is a research professor at the SCP, GIT. His research covers broad area of computing systems (hardware & software), cybersecurity and machine learning. He previously served as Chief Innovation Officer for the ICSD of GTRI. Before joining GTRI, he managed basic and applied science research in cyber security and complex software for ONR where he developed several novel concepts. Prior to ONR, he was a system & chip architect and an entrepreneur in Silicon Valley. He received his Ph.D. in electrical engineering from SUNY-Binghamton
Formal methods is rigorous mathematical representation of an abstracted behavior of a program, usually derived from the program formal specification. Formal methods can verify & guarantee software behavior in a manner that testing cannot. Generally formal verification is performed offline before a program is deployed. Formal model can also be used to enforce program behavior, dynamically, in the form of dynamic (formal) model checking. Dynamic formal model checking can potentially be used to enforce the behavior of COTS executable. Dynamic formal model checking requires mechanism for executing the formal model synchronously with the execution of the COTS program. Georgia Institute of Technology's CSAFA labs developed MonT, a hardware assisted realtime/online program execution monitoring at instruction level granularity at the nominal speed of the main (observed/monitored) processor. MonT has been demonstrated to be capable of stopping 11 CVEs of various types (buffer overflow, integer overflow, use after free), before the exploit can complete. MonT demonstrates that online monitoring of program execution at instruction level granularity and at speed is indeed feasible and practical. As formal model can generally be transformed into state machine, MonT can support formal model checking, in real-time without requiring any software instrumentation.

Secure High-Assurance Aberdeen Architecture RISC-V Complier and Softcore (SHAAARCS)

Dr. Michael Doran DornerWorks
Michael Doran brings over a decade of experience as an embedded software engineer, specializing in high-assurance designs across ARM, x86, and RISC-V platforms. Beyond his professional work, he is pursuing a Ph.D. in Computer Engineering at Georgia Tech, focusing on cybersecurity for hardware devices for critical infrastructure. As a Cyber Warfare Officer in the Army Reserve, Michael has firsthand experience executing missions in this domain, providing him with unique insight into real-world cyber threats. His combined expertise in engineering, research, and military operations drives his commitment to advancing secure computing for mission-critical systems.
Modern cybersecurity relies on a layered defense approach, incorporating leastprivilege and continuous monitoring. However, microprocessors prioritize performance over security, lacking hardware-level enforcement of these principles, leaving them vulnerable to attacks like Spectre and Meltdown. The Aberdeen Architecture addresses these gaps by introducing hardware state machines that enforce four security policies: (1) instruction execution, (2) page memory access, (3) control flow integrity, and (4) data flow integrity. These state machines operate independently of the processor pipeline, employing local policies for finegrained instruction-level security and global policies to limit fault propagation, balancing security and performance. This work explores integrating instruction mediation—an element of the Aberdeen Architecture—into an open-source RISC-V processor (e.g., RocketChip). By evaluating RISC-V toolchains for implementing a two-level tagged architecture, necessary modifications were identified for user-defined tags and security policies. Embedding a hardwarestate machine into the processor and mapping out toolchain adaptations provides a blueprint for realizing the Aberdeen Architecture. This approach strengthens security at the hardware level, mitigating vulnerabilities and laying the foundation for more resilient computing systems.

Hardware Attacks and Defenses for High Assurance Systems

Dr. Sean Zhou Trusted Science and Technolog
Dr. Sean Zhou is a Principal Scientist at Trusted ST specialized in hardware security, computer architecture, and hardware-software codesign. Before Trusted ST, Dr. Zhou has worked at Intelligent Automation Inc. (IAI) and University of Hawaii. He has been PI and technical lead for more than 20 SBIR and BAA programs funded by DARPA, DOD, NASA, DOE, DHS. Particularly relevant to the proposed effort, Dr. Zhou is currently working as the PI for one DARPA SBIR project on hardware side channel attacks, two Army SBIR projects on secure hardware architecture, and one DHS SBIR projects on hardware-assisted malware detection framework.
This presentation reports on our experience with evaluating hardware attack anddefense techniques for high assurance systems. One the offense side, we evaluated both analog side-channel attacks and microarchitectural side-channel attacks, and their impacts to secure architectures including Intel SGX, ARM Morello, and seL4 microkernel. On the defense side, we are developing hardware-software codesign architecture by extending RISC-V cores and seL4 microkernel for security isolation. Such security enhancement can systematically integrate security policy enforcement and isolation at both the software and hardware levels against a variety of hardware side channel attacks. We will briefly introduce state-of-the-art hardware sidechannel attack techniques and provide some background on secure hardware architectures. We will discuss our experiences on RISC-V Instruction Set Architecture (ISA) extensions and integration with seL4 microkernel on FPGA platforms. We will also present our works on hardware-assisted malware detection techniques by leveraging hardware performance counter (HPC) traces to detect ransomware attacks in real time. We will conclude with our visions on secure hardware architecture design including hardware Trusted Computing Base (TCB) and hardware level security policy enforcement for high assurance systems.

Kry10 OS - Trustworthy, Dynamic, and Easy To Use

Dr. Ihor Kuz Kry10
Dr Ihor Kuz is a principal operating system engineer at Kry10, helping develop the Kry10 OS and Platform. Ihor has previous experience leading the team developing the seL4 microkernel, and has been involved with seL4 for as long as it’s been around. Ihor is a member of the seL4 Foundation's technical steering committee (TSC). In the past he has been an associate professor at UNSW in Australia and has taught operating systems, distributed systems and Erlang there for many years.
We present and demonstrate the Kry10 Operating System (KOS). KOS is a newoperation system platform that we are developing at Kry10. It is based on seL4 and builds up a trustworthy foundation, utilising seL4's verified properties to provide a powerful, dynamic, and easy to use OS platform for securing critical systems. Besides providing secure isolation and communication between OS components, KOS also provides: dynamic software update, virtualisation and containerisation support, support for various runtime environments (including freestanding and hosted (semi-POSIX) C, Elixir/Erlang, and Rust), a management subsystem, remote graphical interface, fleet management server, and more. Furthermore, we are in theprocess of adding multicore support and formally verifying the core KOS runtime system. > In this presentation we will introduce Kry10 and its mission, present the Kry10 OSarchitecture, and provide demonstrations of some of its key features, incuding its development environment, dynamic updates, visualisation, and remote management as well as some of the systems we have developed using it.

LITESHIELD: A Lightweight Userspace µKernel Architecture for Secure Container Isolation

Dr. Hui Lu University of Texas at Arlingto
Dr. Hui Lu is an Assistant Professor at the University of Texas at Arlington (UTA). His research focuses on operating systems, virtualization, cloud computing, and network systems. He has collaborated with top labs like Intel Labs, HPE, and AFRL, 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.
We introduce LITESHIELD, a lightweight and secure isolation framework forcontainerized applications for commodity kernels (e.g., Linux). By decoupling traditional guest kernel functions into modular userspace microkernel (µkernel) services, LITESHIELD reduces the reliance on host kernel syscalls from 300+ to just 28, achieving a thin user-to-host interface comparable to virtual machines (VMs). Leveraging fast, shared-memory-based inter-process communication (IPC), LITESHIELD eliminates the need for hypervisors and minimizes costly kernel context switches, reducing the virtualization stack's complexity and attack surface. Its modular design enables seamless integration of specialized userspace services, such as networking and filesystems, while maintaining compatibility with legacy Linux applications through dynamic syscall interception. Performance evaluations show that LITESHIELD matches or exceeds traditional container and VM-based isolation mechanisms in syscall latency, I/O efficiency, and networking throughput. This architecture is particularly suited for cloud-native environments, enabling secure and efficient multi-tenancy while supporting diverse application needs with composable µkernel services. By reimagining container security and performance, LITESHIELD offers a promising alternative to traditional hypervisor-dependent approaches.

Unikernels: A DevSecOps alternative to containers

Robbie VanVossenDornerWorks
Robbie is an employee of DornerWorks, has 12 years of experience in embedded hypervisors, and 10 years of experience with the seL4 microkernel. His work and leadership led to the development of aarch64 virtualization support across the seL4 ecosystem, both in the microkernel and the user-space libraries. He has also developed multiple projects using the Rust language, including embedded implementations of device drivers and applications. He has strong interests in embedded security, virtualization, seL4, and Rust
A Unikernel is a specialized image that contains a single application, a minimalkernel, and the drivers, stacks, and libraries needed for that application. They are mostly used on hypervisors and trade general purpose operation for very small images which results in a smaller attack surface, faster boot times, and lower memory utilization. Since many Unikernels can run on both hypervisors and Unix it has similar DevSecOps benefits as containers, such as being able to easily test applications before deploying them as virtual machines on a target, but with the added benefit of requiring less resources and shorter boot times. In this talk, I will discuss the benefits and drawbacks of using Unikernels in high-assurance security systems and contrast their use against containers for DevSecOps. I will discuss some modern Unikernels which have their own build/orchestration tools and package repositories and how these tools can even integrate with containers. I will also demo some Unikernels running on a host machine and running on top of the secure seL4 hypervisor on embedded target platforms and talk about the porting effort. The talk will conclude with a discussion on next steps for Unikernels in high-assurance systems.

Mobile Software Understanding for Compound Vulnerabilities Using Knowledge Graph (KG) and Graph Neural Network (GNN)

Fei Sun Leidos
Fei Sun is a Cyber Systems Engineer and the Principal Investigator for the Cyber Internal Research and Development project at Leidos Innovations Center. Before joining Leidos, Fei was a Robotics Systems Engineer and Principal Investigator in the Artificial Intelligence and Autonomy Innovation Center at MITRE.
Mobile applications present unique security challenges due to dynamic executionenvironments. Traditional vulnerability analysis often struggles with obfuscated or deeply embedded security threats in mobile software. Our approach leverages AI-based analytics and continuous learning of vulnerability, patch, advisory, and threat data to improve modeling and validation of compound vulnerabilities. Applying our novel Network Path Traversal (NPT) technique to augmented vulnerability analysis and modeling enables accurate, automated exposure and quantification of attack surfaces. Furthermore, we extend existing vulnerability research to refinement, synthesis, and forecasting of mobile exploit sequences through a continuous-learning workflow that feeds validation results back into the GNNs. To gain a deeper understanding of compound vulnerabilities, we use KG to model complex interdependencies between system components to expose attack surfaces and advance the understanding of effectiveness for individual vulnerability in the sequence. We use GNN foundational model for AI/ML-based analysis, using inference development to gain insights into compound vulnerabilities. Using LLM, we further enrich the process of rapid ingestion and actionable threat reports, alerts, and patch advisories. Finally, a continuous learning stream consumes all feedback from any point in the process and feeds into the GNN, for continuous quantitative improvement in analysis efficiency and accuracy.

Secure Robotic Operating System (seROS)

Nathan Studer DornerWorks
Nathan Studer has worked on high assurance software and custom logic applications for 20 years with a focus on embedded virtualization. He obtained his undergraduate degree in Electrical Engineering from Calvin College and has a master’s degree from Michigan State University in Computer Science. Nathan is a Technology Strategy Lead for DornerWorks leading the team in designing systems that meet customer’s security requirements using an appropriate blend of software, hardware, and/or software that emulates hardware. His combined expertise in embedded software, custom logic, and cybersecurity help him deliver practical solutions to the Department of Defense’s difficult cybersecurity challenges.
ROS (Robotic Operating System), a modular componentized architecture for robotapplications, has made it possible to quickly develop and deploy systems utilizing autonomous or human guided robots. Recognizing the benefits of this approach, the Army has created a collection of military specific ROS components to enable autonomy features now called the Army Robotic Common Software (ARCS). While ROS components developed by the Army themselves can be thoroughly vetted, visibility into third party components may be lacking. Furthermore, ROS depends on many services included in a full Linux distribution to function properly leaving a large attack surface. To address these challenges, the Cybersecurity for Robotic & Autonomous Systems Hardening (CRASH) Joint Capabilities Technology Demonstration was created to develop a comprehensive cybersecurity software solution tailored for robotic and autonomous systems. This presentation will provide an overview of this program, how a trusted microkernel/hypervisor such as seL4 can be used to retrofit security features, and suggest a roadmap for future work.

Building a Memory Safe Software Ecosystem with CHERI

Brooks Davis SRI
Brooks Davis is a Principal Computer Scientist at SRI. Since 2012 he has worked on the CHERI project and leads development of the CheriBSD operating system. Prior to joining SRI, he worked on high-performance computing and networking at The Aerospace Corporation. He holds a Bachelor's Degree in Computer Science from Harvey Mudd College. Brooks has been a member of the open-source FreeBSD operating system project since 2001 and has served on the project's elected core team. He is also a Visiting Research Fellow at the University of Cambridge Department of Computer Science and Technology (Computer Laboratory).
CHERI makes it possible to impose strong memory safety and compartmentalization on existing, memory unsafe C and C++ code bases with reasonable effort. Ported software includes hypervisors (seL4), operating systems (Linux, FreeBSD), desktop environments, and even the Chromium web browser. The corpus of code includessome of the most complex open source software in the world consisting of tens of millions of lines of code. While the effort to port it was non-trivial, it pales in comparison to the effort required to write it or (in many cases) even maintain in. With the imminent availability of commercial hardware platforms, CHERI gives us hope for the billions of lines of C and C++ software underpinning critical systems today.

Fine-Grained Security Control through Combined Memory Access Protection and Isolation

Dr. Thomas Wahl Trusted Science and Technology
Dr. Thomas Wahl is a Senior Principal Scientist at Trusted ST. Dr. Wahl received a PhD degree from the University of Texas at Austin in 2007. His expertise lies in model-based formal approaches, specifically in foundational and practical aspects of formally modeling program or system artifacts, and in the scalability of model-based analyses. Particularly relevant to the proposed effort, Dr. Wahl is currently working as the PI for the DARPA INGOTS BAA on vulnerability and exploit modeling, and leading Trusted ST’s effort for the DARPA V-SPELLS BAA on code identification and software analysis for security hardening.
This presentation reports on our experience with implementing fine-grained softwaresecurity control, by combining intra-process memory access protection through Capability Hardware Enhanced RISC Instructions (CHERI) architectures like ARM Morello with interprocess protection through memory isolation. The experience stems from work supported by DARPA’s STO and MTO offices on securing a Swarm Unmanned Aerial Vehicle (SUAV) application, but it has wide-ranging implications beyond the Swarm effort. We will briefly introduce forms of fine-grained security control and provide some background on CHERI, ARM Morello, and seL4 to set the stage. We will share some key lessons learned from work related to porting applications to the Morello system and building security and resilience on top of it, which may benefit communities working along similar lines. We will conclude with some futurevisions and steps, such as automated Cherification and improved fault handling, which, in our experience, are essential to improve the adoption prospects of combined Capability hardware and memory isolation. The ARM Morello architecture on top of which this work was performed is by now a fairly mature technology; it is time to undertake efforts to make it more widely accessible and practically viable.

Exploring Next-Generation Hardware Platforms to Harness the Benefits of CHERI Experimental Implementations

Dr. Hui Zeng PJR Corp
Dr. Hui Zeng is Director at P & J Robinson Corporation (PJR). Dr. Zeng received his Ph.D. in Electrical Engineering from the University of Maryland at College Park. He has extensive experience in networks, security, communications, and applications. His research interests include cyber security, AI/ML, signal processing, networking, wireless network, and tactical cloud. At PJR, Dr. Zeng has played a pivotal role in technology development, team management, business growth, as well as in shaping technical vision and creating strategic roadmaps. Prior to PJR, he was Associate Director (Acting Director) of the Networks & Security division at Intelligent Automation, Inc.
Despite rigorous software testing, exploitable software vulnerabilities frequentlyarise from memory issues. While memory-safe languages like Rust offer greater inherent memory safety, they do not provide absolute protection against such vulnerabilities and cannot soon replace the extensive body of C/C++ code. A hardware approach called CHERI (Capability Hardware Enhanced RISC Instructions) has shown promise in effectively addressing multiple memory safety issues using an ARM Morello prototype. However, several hardware enhancements are still needed to fully harness the benefits of CHERI’s experimental implementations. To address this need, P&J Robinson Corporation (PJR), along with its subcontractors, isexploring the design and development of next-generation hardware platforms to harness the benefits of selected CHERI hardware prototypes like ARM Morello. The goal of our effort is to improve cost efficiency, compactness, modularity, scalability, interoperability and supply chain reliability while maintaining the same “CHERI” features for enhanced security. Towards this goal, we have achieved preliminary results in the testing and evaluation of off the-shelf PCIe cards integrated with the current Morello board, and the initial design of an extension board to support existing and evolving CHERI boards.

SWITCHing to CHERI -- Smoothing the Path to Cyber Security

Dr. David MuslinerSmart Information Flow Technologies (SIFT)
Dr. David Musliner is a senior Technical Fellow at Smart Information Flow Technologies (SIFT), specializing in AI for highly autonomous systems ranging from cyber security reasoning to uncrewed ground, air, and space vehicles.
Two types of cyber security flaws are responsible for the vast majority of all highseverity software vulnerabilities: memory safety failures and over-privilege. CHERI (Capability Hardware Enhanced RISC Instructions) extends conventional processor Instruction-Set Architectures with architectural capabilities to enable fine-grained memory protection and highly scalable software compartmentalization. When used correctly, the CHERI enhancements allow a computer's hardware to reliably prevent memory safety flaws and enforce least-privilege compartmentalization. However, developing software that uses the CHERI enforcement mechanisms remains a challenge, requiring highly-skilled developers with detailed CHERI experience. SIFT's new SWITCH project will mature the tool chain required to build CHERI-compatible software, so that porting existing software is much easier, and developing newsoftware is no harder than on other common computing platforms. This will lower the bar for adoption of memory-safe, capability-enforcing systems, catalyzing dramatic improvements in software security.
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.