vault backup: 2025-02-14 18:03:23

.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
 }

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]

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

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"}
+	]
 }