Visible to the public KU SoS Lablet Quarterly Executive Summary - 2022 Q1Conflict Detection Enabled

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 to explore various microarchitectural attack and defense techniques on Intel and ARM platforms.  Their paper "Denial-of-Service Attacks on Shared Resources in Intel's Integrated CPU-GPU Platforms" was recently accepted for publication at IEEE ISORC 2022.

  • Dr. Prasad Kulkarni and his team continued to develop techniques that detect secure coding practices used in high-level programs by examining binary executables.  In addition, they continued work assessing effectiveness of control flow integrity checks on binary vs. source code.

  • Dr. Perry Alexander and his team expanded upon work examining the semantics of attestation to examine the relative strengths of attestation protocols.  They continued work integrating TPM 2.0 into their attestation manager and integrating with blockchain for provenance using health records and attestation evidence.

B. Community Engagement(s)

The Kansas Lablet played host to FBI Director Christopher Wray and Kansas Senator Jerry Moran.  They toured our facility and were briefed on Lablet research and other defense-related research going on at KU.  Together with Dr. Doug Girod, KU Chancellor, they held a public panel discussion on cybersecurity, the importance of cybersecurity research, and cybersecurity education.  There were well over 200 attendees physically and included most of our research sponsors and our industrial advisory board.  

The Kansas faculty received notification that our NSA/DHS Center for Academic Excellence - Education was renewed.  Drs. Fenjun Li and Bo Luo lead the KU team that prepared the application.  This is our second renewal.  We intent to renew our CAE - Research designation when appropriate.

KU PIs confirmed that our GenCyber funding is being renewed for 2022. GenCyber brings high school teachers to campus for a week-long intensive introduction to cyber security.  GenCyber was put on hold during the pandemic, but in-person workshops are planned for 2022.

KU continues is Lambda Circle reading group for students and faculty interested in languages and security issues.  Recent topics include automated verification of Nakayama's Lemma and contiguity types.  Our work with Nakayama's Lemma is an interdisciplinary effort with the KU Math Department and represents the first known automated proof of this commutative algebra theorem.  A paper is forthcoming.

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

C. Educational Advances

Dr. Perry Alexander agreed to run the first formal methods education panel at the upcoming High Assurance Software and Systems symposium.  Participants include Kevin Hamlem (UT Dallas), Marijn Heule (CMU), Pete Manolios (Northeastern), and Yan Shoshitaishvili (ASU).  The panel will be held on Tuesday, May 17 and will feature short presentations and a discussion of issues related to formal methods education for both undergraduate and graduate students.