A blog for thoughts, technical discussions, announcements.
30 Aug 2021
“Design and Formal Verification of a Copland-based Attestation Protocol” by Adam Petz, Grant Jurgensen, and Perry Alexander has been accepted for publication at the MEMOCODE ‘21 conference, Nov 20-22, to be held virtually. This paper introduces a workflow for both analyzing and executing Copland-based attestation protocols in the context of a security architecture. It concludes by instantiating that workflow with a concrete architecture and layered attestation protocol designed for a DARPA CASE demonstration platform that hosts a legacy UAV flight control application. Here is a link to the camera-ready pdf.
NFM ‘21 (Virtual) Conference Presentation
28 May 2021
I recently presented our work entitled “An Infrastructure for Faithful Execution of Remote Attestation Protocols” at the (virtual) NASA Formal Methods (NFM’21) conference. A video recording of my talk/slides and live Q&A following the talk can be viewed on Youtube here. Here is a link to a pdf of the published paper.
24 Feb 2021
Our paper entitled “An Infrastructure for Faithful Execution of Remote Attestation Protocols” was accepted to appear in the upcoming NASA Formal Methods conference. I will present this work (virtually) during the conference program in May, 2021. Here is a link to the published pdf.
07 Dec 2020
I encountered some surprising (to me) behavior while writing an Ltac procedure involving a “with” clause. A minimal example appears below. The problem occurs when binding a variable from a hypothesis, then using that variable in the LHS of a with binding in the Ltac body. My expectation is that the LHS (x in the assignment x:=y) is unaffected by substitution, and must simply match the name of a bound variable in the type of the Lemma to which it is being applied.
07 Dec 2020
I’ve been listening to “Deep Field” by Eric Whitacre. Inspired by the Hubble Telescope’s Deep Field image. I’d recommend listening on a music streaming service for best sound quality, but here’s a site with a description and companion video with Hubble images: https://deepfieldfilm.com/
24 Nov 2020
I would like to pass a tactic as a parameter to a separately-defined Ltac procedure. However, it seems whenever I include a “;” in that tactic I’m met with a syntax error. I’ve crafted a minimal example below. Perhaps I’ve made a silly mistake with parentheses or some such, but I can’t seem to get it working.
Ltac my_tac tac := tac.
Lemma foo : (1 = 1 /\ 2 = 2).
Proof.
split; [reflexivity | reflexivity]. (* Succeeds as expected *)
Undo.
my_tac (split; [reflexivity | reflexivity]). (* Syntax Error? *)
Qed.
HotSoS 2020 Poster Presentation
22 Sep 2020
Gave a virtual poster presentation at HotSoS 2020 entitled: “An Infrastructure for Faithful Execution of Remote Attestation Protocols”. The poster pdf is here, and the accompanying 3-minute lightning talk presentation here. Fielded live questions from the audience via video chat after.
14 Aug 2020
Passed the oral defense component of my dissertation proposal entitled: “An Infrastructure for Faithful Execution of Remote Attestation Protocols”. Now on to more publications and defending the dissertation!
HotSoS 2019 Paper Presentation
12 Apr 2019
Successfully presented our work entitled “A Copland Attestation Manager” published at HotSoS 2019 (Hot Topics in Science of Security) in Nashville, TN. Watch the presentation on YouTube here: https://youtu.be/vr8FgOt_oVY. The work is co-authored with my advisor, Dr. Perry Alexander, and the full paper can be found here: link to pdf.