ASN1* : Provably Correct Non-Malleable Parsing for ASN.1 DER

EverParse.fst.config.json

@@ -1,16 +1,19 @@
 {
     "fstar_exe": "fstar.exe",
     "options": [
-      "--max_fuel", "0",
+      "--initial_fuel", "0",
+      "--max_fuel", "2",
+      "--initial_ifuel", "2",
       "--max_ifuel", "2",
       "--initial_ifuel", "2"
     ],
     "include_dirs": [
-      "./src/lowparse", 
+      "./src/lowparse",
       "${KRML_HOME}/krmllib",
       "${KRML_HOME}/krmllib/obj",
       "./src/3d",
-      "./src/3d/prelude"
+      "./src/3d/prelude",
+      "./src/ASN1"
     ]
   }
 

Makefile

@@ -1,11 +1,14 @@
-all: quackyducky lowparse 3d
+all: quackyducky lowparse 3d asn1
 
 lowparse:
 	+$(MAKE) -C src/lowparse
 
 3d: lowparse
 	+$(MAKE) -C src/3d
 
+asn1: lowparse
+	+$(MAKE) -C src/ASN1 verify
+
 quackyducky:
 	+$(MAKE) -C src/qd
 
@@ -25,6 +28,9 @@ lowparse-unit-test: lowparse
 
 3d-test: 3d-unit-test 3d-doc-test
 
+asn1-test: asn1
+	+$(MAKE) -C src/ASN1 test
+
 lowparse-bitfields-test: lowparse
 	+$(MAKE) -C tests/bitfields
 
@@ -44,7 +50,7 @@ quackyducky-sample0-test: quackyducky lowparse
 
 quackyducky-test: quackyducky-unit-test quackyducky-sample-test quackyducky-sample0-test quackyducky-sample-low-test
 
-test: all lowparse-test quackyducky-test 3d-test
+test: all lowparse-test quackyducky-test 3d-test asn1-test
 
 ci: test
 
@@ -60,7 +66,7 @@ clean-quackyducky:
 clean: clean-3d clean-lowparse clean-quackyducky
 	rm -rf bin
 
-.PHONY: all gen verify test gen-test clean quackyducky lowparse lowparse-test quackyducky-test lowparse-fstar-test quackyducky-sample-test quackyducky-sample0-test quackyducky-unit-test package 3d 3d-test lowparse-unit-test lowparse-bitfields-test release everparse 3d-unit-test 3d-doc-test ci clean-3d clean-lowparse clean-quackyducky
+.PHONY: all gen verify test gen-test clean quackyducky lowparse lowparse-test quackyducky-test lowparse-fstar-test quackyducky-sample-test quackyducky-sample0-test quackyducky-unit-test package 3d 3d-test lowparse-unit-test lowparse-bitfields-test release everparse 3d-unit-test 3d-doc-test ci clean-3d clean-lowparse clean-quackyducky asn1 asn1-test
 
 release:
 	+src/package/release.sh

src/ASN1/.gitignore

@@ -0,0 +1 @@
+*.checked