KU SoS Lablet Quarterly Executive Summary - 2022 Q2

A. Fundamental Research

The University of Kansas Lablet continued work on four projects targeting resiliency, preventing side channel communication, developing semantics and infrastructure for trust, and secure native binary execution. Specifically, we are: (i) reducing micro-architectural side-channels by introducing new OS abstractions while minimally modifying micro-architecture and OS; (ii) developing an epistemology and ontology for framing resilience; (iii) formalizing the remote attestation and defining sufficiency and soundness; and (iv) developing a framework for client-side security assessment and enforcement for COTS software.

Highlights from this quarter include:

• Dr. Heechul Yun and his team continued continued to develop various microarchitectural attack and defense techniques on Intel and ARM platforms Their paper, "A Closer Look at Intel Resource Director Technology (RDT)," was accepted and published at RTNS 2022. This work shows generational differences in Intel's RDT feature over two generations of Intel's processor designs. 
• Dr. Prasad Kulkarni and his team continued to develop techniques that can detect the presence of secure and recommended coding practices adopted during the (source level) coding stage from just the binary code.  They continued their work to assess the effectiveness and efficiency of conducting control-flow integrity (CFI) on binary code as compared to performing CFI on source code.
• Dr. Perry Alexander and his team continued development of protocol negotiation and synthesis techniques, Initiated formal specification of attestation system manifests for defining and reasoning about complex attestation systems, and began Iformal specification of information disclosure from attestation protocol execution. They continued integrating the TPM 2.0, TSS and OpenSSL into the Copland attestation framework and continued development of attestation health records and initialization focusing on enterprise attestation and supply chain protection.

B. Community Engagement(s)

The Kansas Lablet hosted the US Army Cyber Advantage Fellows for a series of research presentations at KU.  The Cyber Advantage Fellows is a program for up-and-coming Army officers that provides an intensive introduction to advanced cybersecurity issues.  The program is run through The Command and General Staff College by KU Lablet Advisory Board Member Peter Li at Ft. Leavenworth.  We are discussing actively embedding fellows from next year's class in KU Lablet projects.

KU continues is Lambda Circle reading group for students and faculty interested in languages and security issues.  Recent topics include program equivalence and Hoare logic in Coq with applications to separation logic.  Presentations and discussions are open to all.

On May 17 Dr. Perry Alexander chaired the first formal methods education panel at the  High Confidence Software and Systems symposium (HCSS'22) sponsored by NITRD.  Participants included Kevin Hamlem (UT Dallas), Marijn Heule (CMU), Pete Manolios (Northeastern), and Yan Shoshitaishvili (ASU).  Our panelists brought expertise ranging from hands-on model checking and theorem proving to mathematical foundations to the discussion. Panelists presented short overviews of their thoughts on formal methods education followed by a lively Q&A session with the audience.  A full day workshop is being planned in association with next year's conference.

KU Lablet PIs continue work with MITRE, JHUAPL, and NSA to develop remote attestation approaches. Joint work from this effort is available at https://www.copland-lang.org including the Copland Collection of utilities and tools, Copland formal semantics, and attestation manager implementations.

C. Educational Advances

N/A