Faculty

• Perry Alexander - Formal methods; trusted computing; design languages; langauge semantics; system-level design.
• Adam Petz - Research Assistant Professor
• Jennifer Lohoefener - Research Assistant Professor

Research Staff

• Ed Komp - Research staff

Students

• Tj Barclay - Verified Coq to CakeML Synthesis
• Sarah Johnson - Attestation Evidence Semantics
• Will Thomas - Attestation Evidence Semantics
• Logan Schmalz - Verified Attestation Manager DevID Establishment
• Ian Harris - Undecided
• Katelyn Accola - Undergradate Research

Alumni

SLDG (University of Kansas) and KBSE (University of Cincinnati) students who have graduated under my supervision.

PhD Graduates

• Dr. Phillip Baraona - VSPEC Formal Semantics - The syntax and semantics of the VSPEC specification language are described. A transformation from single and multi-component specifications to Larch Shared Language specifications is defined to provide language syntax. Component specifications are defined using the canonical axiomatic style extended to represent component activation. Interconnected components are modeled using CSP to model control.

• Dr. John Penix - Formal Component Retrieval and Architecture Representation - A technique for efficient, correct retrieval of components and a theory of architectures is presented. The component retrieval system combines faceted retrieval and specification matching. Facets are formally defined and extracted from component specifications using forward inference. Retrieval based on facets culls the solution space making specification matching feasible. Architecture theories are used to compose and adapt specifications.

• Dr. Murali Rangarajan - VSPEC formal analysis using automatically generated proof obligations - Defined and implemented a methodology for automatically generating a discharging proof obligations from VSPEC specifications. The semantics of VSPEC were encoded in PVS and proof obligations to test several classes of interface errors generated. Automatic proof scripts are generated with the obligations to attempt automated verification.

• Dr. Cindy Kong - Formal Semantics for Model-Based Specification - Defined a formal semantics for model-based specification and a denotation for the Rosetta specification language to that formalism. The system is based on using hidden algebras to represent abstract state allowing refinement in specification domains.

• Dr. Garrin Kimmell - System Synthesis from a Monadic Functional Language - Defined a methodology for synthesizing globally asynchronous, locally synchronous (GALS) implementations in VHDL and C++ from a common, monadic specification. The specification language, called Oread, uses monadic constructs to represent various computational features.

• Dr. Nick Frisby - Reducing the Cost of Precise Types - Developed a technique for automatically synthesizing precise types for interfaces between stages in language processors. The technique enables composing strongly typed language processing components into compilers and interpreters.

• Dr. Mark Snyder - Type Directed Specification Refinement - Developed techniques for advanced type checking for dependently type Rosetta specifications. Rosetta type checking for dependent types describe partial correctness that in turn guides refinement of specifications towards fully checkable types.

• Dr. Jennifer Streb - A Methodology for Automated Verification of Rosetta Specification Transformations - Developed a theory for describing Rosetta specifications as a lattice of co-algebras. The lattice supports transforming specifications from one domain to another using a Galois Connection as a basis for verifying transformations.

• Dr. Wesley Peck - Model Transformation for Hardware/Software Co-Design - Design space exploration using automated synthesis. Starting with abstract Rosetta specifications, synthesized different implementations using alternative architectures and technologies. The results allow exploration of design alternatives while maintaining abstraction in specifications.

• Dr. Evan Austin - Theorem Provers as Libraries - An Approach to Formally Verifying Functional Programs - Developed an LCF-style theorem proving system in Haskell. Staring with HOL-Lite as a model, developed a set of libraries that implement a DSL for theorem proving over the Haskell Core. The result is a capability supporting verification of Haskell programs in Haskell.

• Dr. Adam Petz - Formally Verified Bundling and Appraisal of Layered Attestation Protocols - Formally defined and verified the Copland Compiler and Copland Virtual Machine for executing Copland protocols to produce evidence. Artifacts are implemented as monadic, functional programs in the Coq proof assistant and verified with respect to a Copland reference semantics that characterizes attestation-relevant event traces and cryptographic evidence shapes. Appraisal soundness is positioned within a novel end-to-end workflow that leverages formal properties of the attestation components to discharge assumptions about honest Copland participants.

• Dr. Anna Fritz - 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.

• Dr. Michael Neises - 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.

MS Graduates

• Megan Peck - Rosetta Composition Semantics - Developed a formal semantics for Rosetta component composition. Each Rosetta model assumes a co-algebraic semantics, thus composition becomes composition of co-algebras.

• Brigid Halling - Towards a Formal Model of the TPM - Developed a formal model of the TPM v1.2 using PVS. Command execution sequencing is done using a state monad to thread state through a command sequence.

• Grant Jurgensen - seL4 Attestation Architecture - Modeling, verifying, and implementation of a seL4-based attestation architecture.

• Drew Cousino - Health Records and Blockchain - Designed and verified a mechanism for storing and retrieving attestation data on the Etherium blockchain.

• Sarah Johnson - Provisioning of TPM DevID Certification - Using Coq to model and verify the provisioning protocols for TPM Initial and Local Device Identifiers.

• Anna Fritz - Type Dependent Policy Language - Using dependent types to statically enforce privacy policy during attestation protocol negotiation.

• Josiah Gray - Implementing TPM Commands In the Copland Remote Attestation Language - Extended Copland to include commands that access a TPM 2.0 using the Microsoft Trusted Software Stack (TSS).

• Paul Klein - Remote Attestation Protocol Verification with a Privacy Emphasis - Developed a form model for attestation protocol execution that accounts for privacy policy and mutual attestation.

• Adam Petz - A Semantics for Attestation Protocols using Session Types in Coq - Developed a verified a semantics for protocols using session types. Defined a small-step execution semantics for protocols typed using dependent session types. Verified execution properties as well as duality among protocol pairs.

• Bharath Elleru - Measuring an Embedded Device - Developed a capability for cataloging software installed on a GUMSTIX embedded processor board. Identifies installed software and determines what installation recipe it is associated with in an attempt to determine if it is legitimate or not.

• Mark Snyder - Modular Type Checking for Rosetta - Defined and developed a type checking system for a subset of Rosetta specifications. Using InterpreterLib, the type checker is implemented as a collection of modular type checking components that are implemented independently.

• Philip Weaver - Reflective Meta-programming in Rosetta - Defined and developed a staged interpreter for the reflective subset of the Rosetta specification language. Established the two-stage nature of Rosetta reflection and augmented the existing expression interpreter to handle quote and unquote terms in expressions.

• Kalpesh Zinjuwadia - GENISYS Component Inversion System - Developed the GENISYS prototype for tracing inputs and outputs for system components back to system inputs and outputs. Generates hierarchies of components and inverts component function to determine desired system input for generating specific component inputs.

• Brandon Morel - SPARTACAS Component Retrieval and Adaptation - Developed the SPARTACAS component retrieval and adaptation building upon feature-based retrieval techniques. Implemented adaptation architectures for automatically performing black box adaptation on partially matching specifications.

• Krishna Ranganathan - Test Vector Generation from Rosetta - Developed a system for representing test requirements in Rosetta and automatically generating test vectors for VHDL systems.

• Srinivas Akkipeddi - Advanced Test Vector Generation from Rosetta - Developed a system for generating WAVES vectors from abstract test vectors. Improved the test vector generation algorithm. Developed mechanisms for specifying and generating test vectors from sampled waveform inputs.

• Cindy Kong - ActiveSPEC-based Active network modeling library - Defined and implemented a collection of PVS libraries for active network modeling. Developed the ActiveNodeSpec library for integrating multiple execution environments into an active node. Verified properties of the active network implementation.

• Sarjoun Doumit - ActiveSPEC and ANSE usage environment using orbit - Developed a combined simulation and formal analysis environment based on the orbit/gravity subsystem. Translated a common graphical representation of active networks into both ANSE and ActiveSPEC representations.

• Makarand Patil - Specification-Based component retrieval using Rosetta - Continued work started by John Penix by implemented a specification retrieval capability using PVS. Demonstrated the capability by developing and fielding a DSP component retrieval library.

• Kshama Jambhekhar - Test Vector Generation from VSPEC - Building on work in the specification-based software testing area, Implemented a specification-based test vector generation tool that transformed VSPEC requirements and entities into abstract test vectors and test scenarios.

• Amit Rajkhowa - VSPEC Constraint Modeling - The semantics of VSPEC constraints are defined in the Performance Description Language (PDL) and a checker implemented. PDL semantics are defined for predefined VSPEC constraints including power consumption, heat dissipation, clock speed, area and pin-to-pin timing. A translator was written to output PDL specifications from the JVOM intermediate form. The translator is integrated into the orbit environment.

• Iqbal Mutabanna - Network security modeling - Techniques for modeling security in active networks is presented. Traditional security models are explored and a proposal for composable security components based on the ActiveSPEC system discussed. Theories describing an FTP file bounce attack are developed and verified. A solution is developed demonstrating that a collection of nodes that are not individually secure can be assembled in a secure fashion within a network.

• Sathiyanarayanan Vijayaraghavan (Sat) - LSL Parsing and PVS Translation - A PCCTS based parser and object model is developed to provide generic front-end analysis for Larch Shared Language (LSL) traits. Semantic checking and symbol table manipulations are provided. The object model is then used to develop a translator from LSL specifications to PVS theories. Shorthands, induction rules, extensionality rules, and other Larch specifics are transformed into PVS their equivalents.

• Tareq Altakrouri - Formal Move Machine Verification - The DSS synthesized design of the Move Machine is formally verified using the Boyer-Moore Theorem proving system. The structural and behavioral representations are translated into Boyer-Moore logic using techniques defined by Hunt. Then, an induction proof is used to show that the structural model meets requirements specified by the behavioral model.

• Raj Sayana - VHDL Partial Evaluation - A partial evaluation system is developed for VHDL. Values are specified for a subset of input parameters and propagated throughout the VHDL code. Dead code is eliminated, loops are unrolled, and wait statements evaluated for validity.

• Liming Cai - Constraint Modeling - Formal theories for constraint modeling are developed using the algebraic specification language COLD-K. These theories model constraint propagation throughout VLSI designs. The theories are translated into the Refine environment and used to evaluate constraints in the COMET co-synthesis environment.

Undergraduates

• Justin Ward - Polytypic Theorem Proving Framework - The Prufrock (literary reference intended) polytypic theorem prover framework. Prufrock was developed to perform static analysis on Haskell and Rosetta source modules. It is a first-order theorem prover supporting rewriting and a proof scripting language.