From b2d4af47292d60aae85d7dd334d94073ef349336 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 4 Oct 2022 16:25:15 +0200 Subject: [PATCH 1/7] add documentation --- README.md | 11 ++++++++++- example/README.md | 0 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 example/README.md diff --git a/README.md b/README.md index 35955356d..4abfc41ea 100644 --- a/README.md +++ b/README.md @@ -39,4 +39,13 @@ Indeed, EverParse is part of [Project Everest](https://project-everest.github.io `make` ### Running -`./bin/qd.exe -help` + +Everparse offers two different executables: + +* `./bin/qd.exe` (or `quackyducky` when using the Docker file in `./example`): this executable produces parser/serializer pairs in F* given an input description similar to C types. + + An example of use of `quackyducky` is detailed in [this documentation]("./example/README.md"). +* `./bin/3d.exe` or (`3d`when using the Docker file in `./example`): this executable produces validators in F* given a description in 3d description language. + + The documentation for this executable can be found [here]("https://project-everest.github.io/everparse/3d.html"). + diff --git a/example/README.md b/example/README.md new file mode 100644 index 000000000..e69de29bb From 2ad15bf6c1a9f7a9fc9ffac3e26711db9bb5ee35 Mon Sep 17 00:00:00 2001 From: Samuel Chassot <14821693+samuelchassot@users.noreply.github.com> Date: Tue, 4 Oct 2022 16:26:36 +0200 Subject: [PATCH 2/7] Update README.md --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 4abfc41ea..b11a78f44 100644 --- a/README.md +++ b/README.md @@ -44,8 +44,8 @@ Everparse offers two different executables: * `./bin/qd.exe` (or `quackyducky` when using the Docker file in `./example`): this executable produces parser/serializer pairs in F* given an input description similar to C types. - An example of use of `quackyducky` is detailed in [this documentation]("./example/README.md"). + An example of use of `quackyducky` is detailed in [this documentation]("../example/README.md"). * `./bin/3d.exe` or (`3d`when using the Docker file in `./example`): this executable produces validators in F* given a description in 3d description language. - The documentation for this executable can be found [here]("https://project-everest.github.io/everparse/3d.html"). + The documentation for this executable can be found [here](https://project-everest.github.io/everparse/3d.html). From 0e10fa9defd2e5e7de663fc1a5ad9a6cc1e4a001 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 4 Oct 2022 17:47:48 +0200 Subject: [PATCH 3/7] continue adding documentation and example --- README.md | 1 - example/Dockerfile | 22 ++++++++++++++++ example/README.md | 51 +++++++++++++++++++++++++++++++++++++ example/build_docker.ps1 | 1 + example/build_docker.sh | 1 + example/files/code/.gitkeep | 0 example/files/specs.qd | 26 +++++++++++++++++++ example/run_docker.ps1 | 2 ++ example/run_docker.sh | 2 ++ 9 files changed, 105 insertions(+), 1 deletion(-) create mode 100644 example/Dockerfile create mode 100644 example/build_docker.ps1 create mode 100644 example/build_docker.sh create mode 100644 example/files/code/.gitkeep create mode 100644 example/files/specs.qd create mode 100644 example/run_docker.ps1 create mode 100644 example/run_docker.sh diff --git a/README.md b/README.md index b11a78f44..2977cfc84 100644 --- a/README.md +++ b/README.md @@ -48,4 +48,3 @@ Everparse offers two different executables: * `./bin/3d.exe` or (`3d`when using the Docker file in `./example`): this executable produces validators in F* given a description in 3d description language. The documentation for this executable can be found [here](https://project-everest.github.io/everparse/3d.html). - diff --git a/example/Dockerfile b/example/Dockerfile new file mode 100644 index 000000000..ae62ad1a9 --- /dev/null +++ b/example/Dockerfile @@ -0,0 +1,22 @@ +# BUILD +## docker build -t customeverparse:everparse . + +# START AND RUN +## docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse && docker exec -it customeverparse /bin/bash + + +FROM projecteverest/everest-linux + +USER root + +RUN ln -s /home/test/everparse/bin/qd.exe /bin/quackyducky +RUN ln -s /home/test/everparse/bin/3d.exe /bin/3d +RUN ln -s /home/test/karamel/krml /bin/krml +RUN ln -s /home/test/FStar/bin/fstar.exe /bin/fstar + +USER test + +ENV FSTAR_HOME="/home/test/FStar" +ENV KRML_HOME="/home/test/karamel" +ENV EVERPARSE_HOME="/home/test/everparse" +ENV LOWPARSE_HOME="${EVERPARSE_HOME}/src/lowparse" diff --git a/example/README.md b/example/README.md index e69de29bb..cc0b0681d 100644 --- a/example/README.md +++ b/example/README.md @@ -0,0 +1,51 @@ +# QuackyDucky example + +This documentation is a walkthrough of the `quackyducky` executable that generates parser/serialiser pairs. + +`quackyducky` is the compiler that generates parsers, serialisers, lemmas and theorems in F* out of a description of a message format. It is described in details in the [USENIX Security 2019 paper](https://www.microsoft.com/en-us/research/publication/everparse/). + +## Walkthrough + +First you have to write a description of the format you want the parser/serialiser for. The format is very similar to C structs. The available types and examples can be found in the [USENIX Security 2019 paper](https://www.microsoft.com/en-us/research/publication/everparse/). + + +As an example, here is a description file: + +``` +struct { + uint16 id; + uint32 list<12..42>; + uint32 list2<32..234>; +} content_one; + +struct { + uint32 size; + uint64 a[size]; +} content_two; + +enum { + one (0x4242), /* Constant tag */ + two (0x4241), + (65535) /* Indicates 16 bit representation */ +} content_type; /* Enum with 2 defined cases */ + +struct { + uint32 id; + content_type c_t; + select (c_t){ + case one: content_one; + case two: content_two; + } inner_content; + uint16 arr[412]; +} message; +``` + +Now, run `./build_docker.sh` (`./build_docker.ps1` respectively) to build the docker image. + +Once it is done, run `./run_docker.sh` (`./run_docker.ps1` respectively) to start a docker container and open a shell inside. + +In the docker container: +- `cd /pwd/files` to go to the `./files` folder next to this README file. +- run `quackyducky -odir code -low specs.qd` command to generate the F* code files in `code` folder. It will generate `.fst` and `.fsti` files that contain the parsers, serialisers and proofs. +- run `cd code && +fstar --z3rlimit 250 --cache_dir cache --cache_checked_modules --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`. \ No newline at end of file diff --git a/example/build_docker.ps1 b/example/build_docker.ps1 new file mode 100644 index 000000000..8db7138aa --- /dev/null +++ b/example/build_docker.ps1 @@ -0,0 +1 @@ +docker build -t customeverparse:everparse . \ No newline at end of file diff --git a/example/build_docker.sh b/example/build_docker.sh new file mode 100644 index 000000000..8db7138aa --- /dev/null +++ b/example/build_docker.sh @@ -0,0 +1 @@ +docker build -t customeverparse:everparse . \ No newline at end of file diff --git a/example/files/code/.gitkeep b/example/files/code/.gitkeep new file mode 100644 index 000000000..e69de29bb diff --git a/example/files/specs.qd b/example/files/specs.qd new file mode 100644 index 000000000..341234134 --- /dev/null +++ b/example/files/specs.qd @@ -0,0 +1,26 @@ +struct { + uint16 id; + uint32 list<12..42>; + uint32 list2<32..234>; +} content_one; + +struct { + uint32 size; + uint64 a[size]; +} content_two; + +enum { + one (0x4242), /* Constant tag */ + two (0x4241), + (65535) /* Indicates 16 bit representation */ +} content_type; /* Enum with 2 defined cases */ + +struct { + uint32 id; + content_type c_t; + select (c_t){ + case one: content_one; + case two: content_two; + } inner_content; + uint16 arr[412]; +} message; \ No newline at end of file diff --git a/example/run_docker.ps1 b/example/run_docker.ps1 new file mode 100644 index 000000000..9f33236f8 --- /dev/null +++ b/example/run_docker.ps1 @@ -0,0 +1,2 @@ +docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse +docker exec -it customeverparse /bin/bash \ No newline at end of file diff --git a/example/run_docker.sh b/example/run_docker.sh new file mode 100644 index 000000000..9f33236f8 --- /dev/null +++ b/example/run_docker.sh @@ -0,0 +1,2 @@ +docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse +docker exec -it customeverparse /bin/bash \ No newline at end of file From b09ad9a3dc9a51b29c185e1c3d0e803525349d51 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 5 Oct 2022 10:50:46 +0200 Subject: [PATCH 4/7] continue working on documentation --- example/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/example/README.md b/example/README.md index cc0b0681d..bbb2c31b1 100644 --- a/example/README.md +++ b/example/README.md @@ -48,4 +48,4 @@ In the docker container: - `cd /pwd/files` to go to the `./files` folder next to this README file. - run `quackyducky -odir code -low specs.qd` command to generate the F* code files in `code` folder. It will generate `.fst` and `.fsti` files that contain the parsers, serialisers and proofs. - run `cd code && -fstar --z3rlimit 250 --cache_dir cache --cache_checked_modules --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`. \ No newline at end of file +fstar --z3rlimit 3000 --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`. \ No newline at end of file From 601f763b7e4736eafed884711662961920a92193 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 5 Oct 2022 10:59:16 +0200 Subject: [PATCH 5/7] documentation --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2977cfc84..904dfa8e9 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,7 @@ Everparse offers two different executables: * `./bin/qd.exe` (or `quackyducky` when using the Docker file in `./example`): this executable produces parser/serializer pairs in F* given an input description similar to C types. - An example of use of `quackyducky` is detailed in [this documentation]("../example/README.md"). + An example of use of `quackyducky` is detailed in [this documentation](./example/README.md). * `./bin/3d.exe` or (`3d`when using the Docker file in `./example`): this executable produces validators in F* given a description in 3d description language. The documentation for this executable can be found [here](https://project-everest.github.io/everparse/3d.html). From 0c70c360e6946d4405c4ed158292b4cd83c5aaf3 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Mon, 10 Oct 2022 09:11:28 +0200 Subject: [PATCH 6/7] add new documentation about example using make --- example/README.md | 18 +++++-- example/files/make_example/.DS_Store | Bin 0 -> 6148 bytes example/files/make_example/Makefile | 45 ++++++++++++++++++ example/files/make_example/Makefile.common | 15 ++++++ example/files/make_example/Makefile.depend | 8 ++++ example/files/make_example/Makefile.qd_files | 4 ++ example/files/make_example/generate_code.sh | 1 + example/files/make_example/specs.qd | 5 ++ example/files/simple_example/.DS_Store | Bin 0 -> 6148 bytes .../files/{ => simple_example}/code/.gitkeep | 0 example/files/{ => simple_example}/specs.qd | 0 11 files changed, 93 insertions(+), 3 deletions(-) create mode 100644 example/files/make_example/.DS_Store create mode 100644 example/files/make_example/Makefile create mode 100644 example/files/make_example/Makefile.common create mode 100644 example/files/make_example/Makefile.depend create mode 100644 example/files/make_example/Makefile.qd_files create mode 100755 example/files/make_example/generate_code.sh create mode 100644 example/files/make_example/specs.qd create mode 100644 example/files/simple_example/.DS_Store rename example/files/{ => simple_example}/code/.gitkeep (100%) rename example/files/{ => simple_example}/specs.qd (100%) diff --git a/example/README.md b/example/README.md index bbb2c31b1..35a15b5e7 100644 --- a/example/README.md +++ b/example/README.md @@ -44,8 +44,20 @@ Now, run `./build_docker.sh` (`./build_docker.ps1` respectively) to build the do Once it is done, run `./run_docker.sh` (`./run_docker.ps1` respectively) to start a docker container and open a shell inside. +## Simple example by hand + In the docker container: -- `cd /pwd/files` to go to the `./files` folder next to this README file. +- `cd /pwd/files/simple_example` to go to the `./files/simple_example` folder next to this README file. - run `quackyducky -odir code -low specs.qd` command to generate the F* code files in `code` folder. It will generate `.fst` and `.fsti` files that contain the parsers, serialisers and proofs. -- run `cd code && -fstar --z3rlimit 3000 --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`. \ No newline at end of file +- run `cd code && fstar --z3rlimit 3000 --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`. + +## Example using make to generate C code + +In the docker container: + +- `cd /pwd/files/make_example` to go to the `./files/make_example` folder next to this README file. +- run `make clean` +- fill `specs.qd` +- run `./generate_code.sh -low` or `./generate_code.sh -high` +- run `make` +- C code is output in the `out` folder diff --git a/example/files/make_example/.DS_Store b/example/files/make_example/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..91dc7d0663d89384418fe90c379a8a5227aa8bd7 GIT binary patch literal 6148 zcmeHKF;2rk5Zp@~$q10#0p0Nf(o&hohzIxs5C@1vEJuh)l>P|~;src`iYM?2DrhK} zy;~d~4x&R5+LiX^ytnI-$0x6kh|Fj)84@K#6vG*N8yHp?ud{coCy_0narZc%T@Lf2 zD(9VC4XmdE{O$%+&>4J6;roj|4#L&4%ChmS8Y3FN-M#D|-aZ|D&zSs@F`u?}$bk19 zMRY~iRMITiJ<0ucd#%m=zIRdxcT-zdOXgMU0q+h!81<>51>FR!=HhX=(&o$`p1(My zuFcq84fxC}^Qoxo6E()M$v&EYpbyNjZ0ac(;fWHqG&X@|;9^Iz{gF6BMBZQq{ z?*8e3mIJ_4u=a=u%=l8EFEw(+FuojdD|xA4?a`N$am=`nFdI3c7{`vdb?IbMk2 .depend + $(FSTAR) --dep full $(QD_FILES) >> .depend + +.PHONY: all \ No newline at end of file diff --git a/example/files/make_example/Makefile.qd_files b/example/files/make_example/Makefile.qd_files new file mode 100644 index 000000000..47a820e8c --- /dev/null +++ b/example/files/make_example/Makefile.qd_files @@ -0,0 +1,4 @@ +all: + echo QD_FILES = $(wildcard *.fst *.fsti) > .qd_files + +.PHONY: all \ No newline at end of file diff --git a/example/files/make_example/generate_code.sh b/example/files/make_example/generate_code.sh new file mode 100755 index 000000000..1ae175566 --- /dev/null +++ b/example/files/make_example/generate_code.sh @@ -0,0 +1 @@ +quackyducky -odir . $1 specs.qd \ No newline at end of file diff --git a/example/files/make_example/specs.qd b/example/files/make_example/specs.qd new file mode 100644 index 000000000..e64ecbf7f --- /dev/null +++ b/example/files/make_example/specs.qd @@ -0,0 +1,5 @@ +struct { + uint64 id; + uint16 size; + uint8 arr[size]; +} message; \ No newline at end of file diff --git a/example/files/simple_example/.DS_Store b/example/files/simple_example/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..5ca0b3803c26735a5a93b0a57fb13af9c3233c9f GIT binary patch literal 6148 zcmeHKy=uci43-)XhAx3D9q$z~cew@!vgZX#;?fQ=mnBd-dFu=Gk@8^q^wW^wy3nQ2 zB7yGnN&0;DH&_-C@#4_ViKawU!v*PGmZ3>rd|)>oseml^*genJ+tTd^mE!^7RA<2R08oD8)o`t|1TaYem>qjVL||-Gpi$XJ3^qFA z$?LLXZ)kL4JsJ1$li4Q}*3%JBT27n|V+{pDfolaOww+4u$(N+x9R*a3b;=7BwB-hAi$KFush$|f!KLVmlSSaut G3Y-9@>n7j; literal 0 HcmV?d00001 diff --git a/example/files/code/.gitkeep b/example/files/simple_example/code/.gitkeep similarity index 100% rename from example/files/code/.gitkeep rename to example/files/simple_example/code/.gitkeep diff --git a/example/files/specs.qd b/example/files/simple_example/specs.qd similarity index 100% rename from example/files/specs.qd rename to example/files/simple_example/specs.qd From 766d6651efffc58dc39b2a438ab3539a9b42f781 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Mon, 10 Oct 2022 09:12:56 +0200 Subject: [PATCH 7/7] missing save --- example/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/example/README.md b/example/README.md index 35a15b5e7..3027d4e7f 100644 --- a/example/README.md +++ b/example/README.md @@ -51,7 +51,7 @@ In the docker container: - run `quackyducky -odir code -low specs.qd` command to generate the F* code files in `code` folder. It will generate `.fst` and `.fsti` files that contain the parsers, serialisers and proofs. - run `cd code && fstar --z3rlimit 3000 --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --include $LOWPARSE_HOME --include $KRML_HOME/krmllib --include $KRML_HOME/krmllib/obj --cmi --expose_interfaces *.fst *.fsti ` to verify the F* code. If the verification times out, you can modify the value of the option `--z3rlimit`. -## Example using make to generate C code +## Example using `make` to generate C code In the docker container: