2022 Summit
Fourth Annual Summit Technical Program
January 31 - February 3, 2022
The fourth Trusted Computing Center of Excellence Summit was held virtually from January 31st – February 3rd, 2022. The four-day packed agenda opened with a day-long set of optional tutorials. HENSOLDT kicked off the event with a tutorial entitled, “Teaser Training seL4, CAmkES and TRENTOS” followed by Kansas State University’s presentation on “Model-based Generation for seL4”. The afternoon sessions were made up of Trusted Science and Technology’s “ARES Secure Kernel on ZCU102 and RTI’s “OMG DDS for Simplifying seL4 Development and Use Cases”.
Approximately 85 government, industry and academia participants from around the globe attended the Summit. After opening remarks from the Summit General Chair Dr. Raymond Richards, the Defense Advanced Research Projects Agency’s (DARPA) Dr. Kathleen Fisher presented her keynote address on “Provable Security: Next Steps to Broader Deployment”. The bulk of the day was focused on efforts underway in national and defense labs with presentations from Air Force Research Laboratory, the Office of Naval Research, Army Combat Capabilities Development Command, DARPA, Sandia Labs, and Idaho National Laboratory. Professor Gernot Heiser then provided a “State of the Union” talk on seL4 and the seL4 Foundation. The day concluded with a panel discussion moderated by Dr. Jason Li and centered around “Proof, Assurance, and Evidence”.
The second day of the Summit’s formal program kicked off with a keynote address from Ian Crone from the Office of the Undersecretary of Defense. He was followed by a hardware focused session with presentations from DARPA, Cambridge University, and Lockheed Martin. Next up were presentations from HENSOLDT, Adventium Labs, and DornerWorks with an emphasis on assured systems. Dr. Raymond Richards from Leidos then gave a special presentation entitled “Survey and Lessons Learned on Separation Kernels”. Day two concluded with a panel moderated by Todd Carpenter from Adventium Labs and addressed “Gaps and Needs” in this technology area.
The final day of the Summit picked up where day two left off with a second session on assured systems and consisted of presentations from the University of Illinois at Urbana-Champaign, North Carolina Agricultural and Technical State University, and HENSHOLDT. Presentations then shifted focus to enclaves and trusted execution with talks by Ohio State University, Binghamton University, Berkeley Lab and UC Davis. That was followed by the third and final session on assured systems with Kestrel, Kansas State University, Adventium Labs, CymanII, and University of Texas San Antonio providing presentations. The Summit then wrapped up a set of talks centered on the seL4 Foundation, the Trusted Computing Center of Excellence, and ongoing technical challenges in the area. Presenters included the SeL4 Foundation, Adventium Labs, Intelligent Automation – A BlueHalo Company, and the Griffiss Institute.
2022 Summit Agenda
Monday, Jan 31 | Tuesday, Feb 1 | Wednesday, Feb 2 | Thursday, Feb 3
Monday, January 31, 2022
Tutorials
Chair & Time Tutorial Opening Patrick Hurley
VideoTutorial #1 – Teaser Training seL4, CAmkES and TRENTOSSebastian Eckl, HENSOLDT 08:30AM – 10:30AMVideoTutorial #2 – Model-Based Code Generation for seL4 10:45AM – 12:45PM
Prof. John Hatcliff & Jason Belt, Kansas State UniversityVideo
Tutorial #3 – ARES Secure Kernel on ZCU102 13:00PM – 15:00PM
Nicholas Evancich, Trusted Science and TechnologyVideo | Presentation
Tutorial #4 – OMG DDS for Simplifying seL4 Development and Use Cases 15:15PM – 17:15PM Paul Pazandak and Fabrizio Bertocci, RTIVideo | Presentation
Tutorial Closing 17:15PM – 17:30PM
Patrick Hurley, Griffiss Institute
Tuesday, February 1, 2022
Chair & Time Session #1 – Introduction and Keynote Dr. Ray RichardsOpening Remarks and Introduction to Keynote Speaker
General Chair, Dr. Ray Richards, Leidos 09:00AM – 09:15AM
Keynote 1: Provable Security: Next Steps to Broader Deployment 09:15AM – 10:15AM
Dr. Kathleen Fisher, DARPA I2O
Presentation | Video: Intro & Keynote | Chat
Break (15 Minutes) 10:15AM – 10:30AM
- Session #2 – Government and Labs Efforts I Dr. Paul Ratazzi
- Mission Assurance in a Cyber Contested Environment Dr. Sarah Muccio, AFRL 10:30AM – 11:00AM
- Coping with the Curse of Complexity Dr. Ryan Craven, ONR 11:00AM – 11:30AM
- Army CCDC-GVSC Vision and Progress Leonard Elliott, Army CCDC-GVSC 11:30AM – 12:00PM
- Reducing Formal Methods to Practice Dr. Brad Martin, DARPA 12:00PM – 12:30PM
Break (30 Minutes) 12:30PM – 13:00PM
- Session #3 – Government and Labs Efforts II Douglas Schafer
- Secure Architecture for Army Mission Critical Systems Tom Barnett, US Army DEVCOM 13:00PM – 13:30PM
- Cyber-Hardened Satellite Software (CHSS) Joseph “Dan” Trujillo, AFRL/RVSW 13:30PM – 14:00PM
- Trusted Systems Research at Sandia Noah Evans, Sandia Labs 14:00PM – 14:30PM
- Properties and Paths from Makers and Breakers Dr. Greg Shannon, Idaho National Lab 14:30PM – 15:00PM
Break (15 Minutes) 15:00PM – 15:15PM
Break (15 Minutes) 16:00PM – 16:15PM
- Session #4 – Proof, Assurance, and Evidence 16:15PM – 17:15PM Moderator: Dr. Jason Li, Program Co-Chair
- Dr. Ray Richards, Leidos
- Prof. Kevin Hamlen, University of Texas at Dallas
- Prof. Gernot Heiser, UNSW and Data61
- Dr. Brad Martin, DARPA
Closing Remarks Douglas Schafer, Cohere Technologies 17:15PM – 17:30PM
Wednesday, February 2, 2022
Chair & Time Session #5 – Introduction and Keynote Introduction to Keynote Speaker Dr. Sukarno Mertoguno, Program Co-Chair, Georgia Tech 09:00AM – 09:15AM
Keynote 2: Ian Crone, OUSD 09:15AM – 10:15AM
Video
Break (15 Minutes) 10:15AM – 10:30AM
- Session #6 – Hardware Technologies I Dr. Jason Li
- How DARPA’s SSITH Program Makes Software More Secure Keith Rebello, DARPA MTO 10:30AM – 11:00AM
- From CHERI to Morello: Capability Hardware Enhanced RISC Instructions 11:00AM – 11:30AM Dr. Robert Watson, Cambridge Universit
- Verified Security Properties and Semantics-Assisted Engineering for the Morello, CHERI-RISC-V, and CHERI-MIPS Capability-Enhanced Architectures Peter Sewell, Cambridge University 11:30AM – 12:00PM
- Directly Integrated and Embedded Hardware Architecture Resilience by Design 12:00PM – 12:30PM Dr. Brian Uhlhorn
Break (30 Minutes) 12:30PM – 13:00PM
- Session #7 – Assured Systems I Dr. Eric Smith
- Porting seL4 to Secure (RISC-V) Hardware Sebastian Eckl, Axel Heider, HENSOLDT Cyber GmbH 13:00PM – 13:30PM
- Model-Based Information Flow Specification and Management for seL4 13:30PM – 14:00PM Todd Carpenter, Adventium Labs
- Accelerating seL4 VMM Development with VM-Composer Michael Doran, DornerWorks, Ltd 14:00PM – 14:30PM
Break (30 Minutes) 14:30PM – 15:00PM
Special Presentation: Survey and Lessons Learned on Separation Kernels Dr. Ray Richards, Leidos 15:00PM – 15:45PM
Introduction by Dr. Lok Yan
Presentation | Video | Chat
Break (15 Minutes) 15:45PM – 16:00PM
- Session #8 – Panel Discussion – Gaps and Needs 16:00PM – 17:15PM Moderator: Todd Carpenter, Adventium Labs
- Dr. Dariusz Mikulski US Army DEVCOM GVSC
- Sascha Kegreiß, HENSOLDT Cyber GmbH
- Nick Evancich, Trusted Science and Technology
- Dr. Valerio Senni, Collins
Closing Remarks Dr. Paul Ratazzi, Air Force Research Laboratory 17:15PM – 17:30PM
Thursday, February 3, 2022
- Chair & Time
- Session #9 – Assured Systems II Kyle Tillotson
- Hardware-Assisted Ransomware Defenses, Detections, and Post-Attack Analysis 09:00AM – 09:30AM Prof. Jian Huang, The University of Illinois at Urbana-Champaign
- Simulating Hardware Faults in seL4 09:30AM – 10:00AM Daniel Limbrick, North Carolina Agricultural and Technical State University
- Edge-to-Center Data Enclaves for Scientific Computing 10:00AM – 10:30AM Olivier Engelkes, HENSOLDT Cyber GmbH
Break (30 Minutes) 10:30AM – 11:00AM
- Session #10 – Enclaves and Trusted Execution Michael Lynch
- Using Symbolic Formal Verification to Identify Security Vulnerabilities in SGX Enclave Programs 11:00AM – 11:30AM Zhiqiang Lin, Ohio State University
- Achieving Both Security of VMs and Speed of Containers in Cloud Native 11:30AM – 12:00PM Prof. Hui Lu, Binghamton University
- Edge-to-Center Data Enclaves for Scientific Computing 12:00PM – 12:30PM Venkatesh Akella and Sean Peisert, Berkeley Lab and UC Davis
Break (30 Minutes) 12:30PM – 13:00PM
- Session #11 – Assured Systems III Todd Humiston
- Correct-By-Construction Generation of C Code for seL4 Networking 13:00PM – 13:30PM Dr. Eric Smith, Kestrel
- Integrated Formal Verification Environment for seL4 Applications 13:30PM – 14:00PM Dr. Robby and Dr. John Hatcliff from KSU, Dr. Danielle Stewart and Todd Carpenter from Adventium Labs
- CADA: CyManII Attack-Defense Annex (Jerry Dussault, Griffiss Institute) 14:00PM – 14:30PM Matthew Jablonski, Duminda Wijesekera, Gabriela Ciocarlie, CymanII and UTSA
Break (30 Minutes) 14:30PM – 15:00PM
- Session #12 – Foundation, Challenges and Center of Excellence Jerry Dussault
- The seL4 Foundation: Progress and Vision 15:00PM – 15:30PM Dr. June Andronick, Proofcraft, seL4 Foundation, and UNSW
- Temporal Isolation with MCS John Shackleton, Adventium Labs 15:30PM – 16:00PM
- I See the ECO, But Where is the System? Dr. Renato Levy, IAI 16:00PM – 16:30PM
- Center of Excellence Progress and Way Forward Patrick Hurley, Griffiss Institute 16:30PM – 17:00PM
Closing Remarks Dr. Brad Martin, DARPA 17:00PM – 17:15PM