formatting

_data/people.yml

@@ -20,10 +20,6 @@
   description: Verified Coq to CakeML Synthesis
   role: student
 
-- name: Michael Neises
-  description: Measurement Using Contextual Inspection
-  role: student
-
 - name: Sarah Johnson
   description: Attestation Evidence Semantics
   role: student
@@ -108,6 +104,9 @@
   description: A Formally Verified Infrastructure for Negotiating Remote Attestation ProtocolsAttestation Protocol Negotiation - Formall defined a negotiation strategy and ordering for Copland protocols. Defined and verified decidability of a static semantics for protocol executability and policy adherence.  Defined and demonstrated an ordering over protocols based on attack graph comparison using Chase and Coq.
   role: phd
 
+- name: Dr. Michael Neises
+  description: Verification-Enabled Runtime Integrity Attestation of Linux (VERIAL)- Runtime attestation is a way to gain confidence in the current state of a remote target. Layered attestation is a way of extending that confidence from one component to another. Introspective solutions for layered attestation require strict isolation. The seL4 is uniquely well-suited to offer kernel properties sufficient to achieve such isolation. We design, implement, and evaluate introspective measurements and the layered runtime attestation of a Linux kernel hosted by the seL4. VERIAL can detect diamorphine-style rootkits with performance cost comparable to previous work.
+
 - name: Grant Jurgensen
   description: seL4 Attestation Architecture - Modeling, verifying, and implementation of a seL4-based attestation architecture.
   role: ms