Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add documentation and example for quackyducky part of Everparse #86

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -39,4 +39,12 @@ 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).
22 changes: 22 additions & 0 deletions example/Dockerfile
Original file line number Diff line number Diff line change
@@ -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"
63 changes: 63 additions & 0 deletions example/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
# 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.

## Simple example by hand

In the docker container:
- `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`.

## 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
1 change: 1 addition & 0 deletions example/build_docker.ps1
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
docker build -t customeverparse:everparse .
1 change: 1 addition & 0 deletions example/build_docker.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
docker build -t customeverparse:everparse .
Binary file added example/files/make_example/.DS_Store
Binary file not shown.
45 changes: 45 additions & 0 deletions example/files/make_example/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
include Makefile.common

all: verify test

cache/%.checked:
$(FSTAR) $(OTHERFLAGS) $<
@touch $@

krml/%.krml:
$(FSTAR) --codegen krml $(patsubst %.checked,%,$(notdir $<)) --extract_module $(basename $(patsubst %.checked,%,$(notdir $<))) --warn_error '@241'
@touch $@

-include .depend

.qd_files: $(QD_FILES)
+$(MAKE) -f Makefile.qd_files

.depend: .qd_files
+$(MAKE) -f Makefile.depend

depend: .depend

verify: $(patsubst %,cache/%.checked,$(QD_FILES))
echo $*

ALL_KRML_FILES := $(filter-out krml/prims.krml,$(ALL_KRML_FILES))

extract: $(ALL_KRML_FILES) # from .depend
mkdir -p out
$(KRML) -warn-error '@2' -skip-compilation $^

test.exe: $(ALL_KRML_FILES)
mkdir -p out
$(KRML) $(LOWPARSE_HOME)/LowParse_TestLib_Low_c.c -no-prefix Test $^ -o test.exe

test: test.exe
./test.exe

%.fst-in %.fsti-in:
@echo $(FSTAR_OPTIONS)

clean:
rm -rf .qd_files .depend cache krml out $(filter-out Test.fst,$(QD_FILES)) test.exe

.PHONY: all depend verify extract clean build test
15 changes: 15 additions & 0 deletions example/files/make_example/Makefile.common
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
FSTAR_OPTIONS = --odir krml --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

FSTAR = $(FSTAR_HOME)/bin/fstar.exe --trace_error $(FSTAR_OPTIONS)

HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"')

KRML = $(KRML_HOME)/krml \
-ccopt "-Ofast" \
-drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \
-tmpdir out \
-bundle 'LowParse.\*' \
$(HEADERS) \
-warn-error -9
8 changes: 8 additions & 0 deletions example/files/make_example/Makefile.depend
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
include Makefile.common
include .qd_files

all:
cat .qd_files > .depend
$(FSTAR) --dep full $(QD_FILES) >> .depend

.PHONY: all
4 changes: 4 additions & 0 deletions example/files/make_example/Makefile.qd_files
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
all:
echo QD_FILES = $(wildcard *.fst *.fsti) > .qd_files

.PHONY: all
1 change: 1 addition & 0 deletions example/files/make_example/generate_code.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
quackyducky -odir . $1 specs.qd
5 changes: 5 additions & 0 deletions example/files/make_example/specs.qd
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
struct {
uint64 id;
uint16 size;
uint8 arr[size];
} message;
Binary file added example/files/simple_example/.DS_Store
Binary file not shown.
Empty file.
26 changes: 26 additions & 0 deletions example/files/simple_example/specs.qd
Original file line number Diff line number Diff line change
@@ -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;
2 changes: 2 additions & 0 deletions example/run_docker.ps1
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse
docker exec -it customeverparse /bin/bash
2 changes: 2 additions & 0 deletions example/run_docker.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
docker run --rm -v $PWD:/pwd -d --name customeverparse -i customeverparse:everparse
docker exec -it customeverparse /bin/bash