From b42702b556953f3dc13ebe1dc85e78303e942590 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 25 Feb 2025 15:33:34 -0500 Subject: [PATCH] vault backup: 2025-02-25 15:33:34 --- .../Weekly Note 2025-02-25.md | 14 ++++++++++++++ 201 Metadata/My Library.bib | 16 ++++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/2 Cole Group Meeting Notes/Weekly Note 2025-02-25.md b/2 Cole Group Meeting Notes/Weekly Note 2025-02-25.md index 055a2c60c..c29bc0cb6 100644 --- a/2 Cole Group Meeting Notes/Weekly Note 2025-02-25.md +++ b/2 Cole Group Meeting Notes/Weekly Note 2025-02-25.md @@ -14,6 +14,20 @@ tags: [] # Last Week's Plan # Accomplishments ## Remarks +### A Myriad of Programming Language Learning +1. Haskell - Did first two chapters of the book. Learned all about set building with predicates, and I'm pretty impressed. The Haskell book made a good point about trimming down solutions, additive vs subtractive manufacturing +2. Lean - I have proved 2+2=4. Successfully explained it to my girlfriend, who hates programming. +3. TLA+ - Watched the first two video lectures. I also got my own set up for writing TLA instead of using the TLA Toolbox. The next video I need to watch is Lamport telling me why I need to use the TLA Toolbox. +### Reading +I've not been learning to write Assembly, but I have been learning about it. +I've read a bit of paper on verifying Assembly code +### Classes +1. ME 2150 - Did microkit part 3 and part 4. Wasn't too bad. Turns out I suck at wordle with 5 tries instead of 6 though. +2. NUCE 2113 - Laboratory 5 - Doing radiation spectrums using sodium iodide detectors +3. ME 2046 - Learned about the w plane. An interesting idea that seems so simple of doing with the inverse of tustin's transform. +### Service +GSA - taught some qualifying exam takers about the state of the art. +Poked Antoine about NUCE classes for the summer, also chatted with Gleeson. Need to email them both. ## Tasks and Notes From This Past Week >[!abstract] Read Papers >```tasks diff --git a/201 Metadata/My Library.bib b/201 Metadata/My Library.bib index cd1ec157c..11af84d85 100644 --- a/201 Metadata/My Library.bib +++ b/201 Metadata/My Library.bib @@ -4518,6 +4518,22 @@ Artiļ¬cial Intelligence Program.pdf} isbn = {0-262-35100-5} } +@article{fromherzVerifiedEfficientEmbedding2019, + title = {A Verified, Efficient Embedding of a Verifiable Assembly Language}, + author = {Fromherz, Aymeric and Giannarakis, Nick and Hawblitzel, Chris and Parno, Bryan and Rastogi, Aseem and Swamy, Nikhil}, + date = {2019-01-02}, + journaltitle = {Source code for Article: A Verified, Efficient Embedding of A Verifiable Assembly Language}, + shortjournal = {Proc. ACM Program. Lang.}, + volume = {3}, + pages = {63:1--63:30}, + doi = {10.1145/3290376}, + url = {https://dl.acm.org/doi/10.1145/3290376}, + urldate = {2025-02-14}, + abstract = {High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system's type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90\% of secure Internet traffic.}, + issue = {POPL}, + file = {/home/danesabo/Zotero/storage/JAJSQPC2/Fromherz et al. - 2019 - A verified, efficient embedding of a verifiable assembly language.pdf} +} + @inproceedings{fultonKeYmaeraAxiomaticTactical2015, title = {{{KeYmaera~X}}: {{An Axiomatic Tactical Theorem Prover}} for {{Hybrid Systems}}}, shorttitle = {{{KeYmaera~X}}},