From 47db7562cea4d1cd6490895290f7aa4efae16108 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Fri, 14 Feb 2025 18:03:23 -0500 Subject: [PATCH] vault backup: 2025-02-14 18:03:23 --- .obsidian/graph.json | 11 ++++- 1000s Templates/Literature Note.md | 14 +++++++ .../fromherzVerifiedEfficientEmbedding2019.md | 42 +++++++++++++++++++ 3-99 Research/Assembly/Assembly Canvas.canvas | 8 +++- 4 files changed, 71 insertions(+), 4 deletions(-) create mode 100644 200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md diff --git a/.obsidian/graph.json b/.obsidian/graph.json index fe2167ec7..a159ab584 100755 --- a/.obsidian/graph.json +++ b/.obsidian/graph.json @@ -5,7 +5,7 @@ "showAttachments": false, "hideUnresolved": true, "showOrphans": true, - "collapse-color-groups": true, + "collapse-color-groups": false, "colorGroups": [ { "query": "path:\"4 Qualifying Exam\" ", @@ -41,6 +41,13 @@ "a": 1, "rgb": 6054102 } + }, + { + "query": "path:\"3-99 Research\" ", + "color": { + "a": 1, + "rgb": 5419488 + } } ], "collapse-display": true, @@ -53,6 +60,6 @@ "repelStrength": 18.0729166666667, "linkStrength": 0.744791666666667, "linkDistance": 177, - "scale": 0.08352472158263505, + "scale": 0.42284390301209, "close": false } \ No newline at end of file diff --git a/1000s Templates/Literature Note.md b/1000s Templates/Literature Note.md index b376f163d..4daee9d2b 100755 --- a/1000s Templates/Literature Note.md +++ b/1000s Templates/Literature Note.md @@ -56,8 +56,22 @@ pages: {{ pages }} | replace('[', '') | replace(']', '') }}{% if not loop.last -%}, {% endif %}{% endfor %} + +{% set in_read = false %} +{% for collection in collections %} + {% if collection.name == "read" %} + {% set in_read = true %} + {% endif %} +{% endfor %} +{{in_read}} + +{% if in_read %} +- [x] {{title}} #Reading ✅ {{ importDate | format("YYYY-MM-DD h:mm a") }} +{% else %} - ["] {{title}} #Reading +{% endif %} + {% if abstractNote -%} >[!Abstract] diff --git a/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md b/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md new file mode 100644 index 000000000..5260836fc --- /dev/null +++ b/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md @@ -0,0 +1,42 @@ +--- +readstatus: false +dateread: +title: "A verified, efficient embedding of a verifiable assembly language" +year: 2019 +authors: + + - "Fromherz, Aymeric" + + - "Giannarakis, Nick" + + - "Hawblitzel, Chris" + + - "Parno, Bryan" + + - "Rastogi, Aseem" + + - "Swamy, Nikhil" + citekey: "fromherzVerifiedEfficientEmbedding2019" +journal: "Source code for Article: A Verified, Efficient Embedding of A Verifiable Assembly Language" +volume: 3 +issue: POPL +pages: 63:1–63:30 +--- +# Indexing Information +## DOI +[10.1145/3290376](https://doi.org/10.1145/3290376) +## Tags: + + +- ["] A verified, efficient embedding of a verifiable assembly language #Reading + +>[!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.>[!seealso] Related Papers +> + +# Annotations +## Notes + +## Follow-Ups + +### Imported: 2025-02-14 5:57 pm diff --git a/3-99 Research/Assembly/Assembly Canvas.canvas b/3-99 Research/Assembly/Assembly Canvas.canvas index f7245215c..3f6fd749b 100644 --- a/3-99 Research/Assembly/Assembly Canvas.canvas +++ b/3-99 Research/Assembly/Assembly Canvas.canvas @@ -1,6 +1,10 @@ { "nodes":[ - {"id":"fd8f3e9ca2c339c1","x":-120,"y":-400,"width":560,"height":540,"type":"text","text":"# What the Hell is Assembly?\n\nWhen a higher level programming language makes its way down to the binary machine-code level, it usually passes through a language called Assembly. Assembly is a very low level language that for the most part has 1:1 combination of assembly commands with machine code equivalents. The important difference between the two is that assembly tries to make things more human readable. Here's an example from Wikipedia:\n\n```assembly\n; Binary Code\n10110000 01100001\n\n; Hex Equivalent\nB0 61\n\n; Assembly Code\nMOV AL, 61h ; Load AL with 97 decimal (61 hex)\n```\n\nNotably, assembly language has a specific dialect for every kind of chip. Because different platforms have different binary codes, the assembly equivalent for one chip will not necessarily work on another. "} + {"id":"fd8f3e9ca2c339c1","type":"text","text":"# What the Hell is Assembly?\n\nWhen a higher level programming language makes its way down to the binary machine-code level, it usually passes through a language called Assembly. Assembly is a very low level language that for the most part has 1:1 combination of assembly commands with machine code equivalents. The important difference between the two is that assembly tries to make things more human readable. Here's an example from Wikipedia:\n\n```assembly\n; Binary Code\n10110000 01100001\n\n; Hex Equivalent\nB0 61\n\n; Assembly Code\nMOV AL, 61h ; Load AL with 97 decimal (61 hex)\n```\n\nNotably, assembly language has a specific dialect for every kind of chip. Because different platforms have different binary codes, the assembly equivalent for one chip will not necessarily work on another. ","x":-120,"y":-400,"width":560,"height":540}, + {"id":"1e4c6175dc1ce2a7","x":-100,"y":260,"width":400,"height":60,"color":"2","type":"text","text":"What does it mean to verify Assembly Code?"}, + {"id":"3c1ca33143d2b5b5","x":-100,"y":460,"width":400,"height":400,"type":"file","file":"200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md"} ], - "edges":[] + "edges":[ + {"id":"3553d8973732e800","fromNode":"1e4c6175dc1ce2a7","fromSide":"bottom","toNode":"3c1ca33143d2b5b5","toSide":"top"} + ] } \ No newline at end of file