proof-read

docs/attack_runs.md

@@ -61,7 +61,7 @@ timeout 600 binsec -config 7.5_1bitflip.cfg
 cd /home/binsec-ase/artefact/benchmarks/dullien_linked/
 binsec -config 7.5_1bitflip.cfg 
 ```
-Here is a shorter version stopping at the first attack found (under 5 s).
+Here is a shorter version stopping at the first attack found (under 1s).
 ```
 binsec -config 7.5_1bitflip_stopFirst.cfg
 ```

docs/new_setup.md

@@ -16,16 +16,16 @@ It is also possible to add a BINSEC directive natively. This is harder to write
 We use the command line ```gcc -Wall -m32 -static -O0 -g source.c -o source.x```.
 - `-m32` flag is to specify a target architecture 32 bits (Intel). Other architecture can be targeted but with less support. This comes with newer version of BINSEC. 
 - `-static` flag includes all library functions statically to the executable. BINSEC does not support dynamic linking.
-- `-O0` flag is to compile without any compile optimization, which can change the program behavior, removing redundant tests for instance. It also improves the readability of the assembly.
-- `-g` flag enabled debug information and is here for convenience, makes it easier to compare assembly code and C code for reasoning on results.
+- `-O0` flag is recommended for convenience to compile without any compile optimization, which can change the program behavior, removing redundant tests for instance. It also improves the readability of the assembly.
+- `-g` flag is recommended for convenience as it enables debug information making it easier to compare assembly code and C code for reasoning on results.
 
 Other compilers can be used as well, as long as necessary behavior flags are used.
 
 # Configuration
 
 To configure BINSEC/ASE, you need to open the target binary with your favorite disassembly software, and look for several informations.
-- where do you want your symbolic execution to start (`entrypoint` option) ? By default, the symbolic execution starts in the main function, you may have some initialization you want to preserve before starting the injection. We recommend to have one injection target interval per function and omit the beginning pushing the return value on the stack. 
-- where is your oracle ? You need the code line adresses of a success and of a failure for `goal-address` and `assert-fail-address` options respectively.
+- where do you want your symbolic execution to start (`entrypoint` option) ? It is usually at `main` in practice.
+- where is your oracle ? You need the code line addresses of a success and of a failure for `goal-address` and `assert-fail-address` options respectively.
 - You may need to load data sections to ensures the initialization of global variables with the SE option `-sse-load-sections .data,.rodata,.bss`, we recommend not doing it if unnecessary as it may also lead to incorrect output. You may also add variables in the memory file to init the SE.
 
 At this stage we recommend a BINSEC/ASE run without any faults, with the `fault-model = None` option. There are two things to check:
@@ -45,21 +45,21 @@ decode-replacement = \
 ```
 
 Now that our program is set for a classic SE run, we can play with adding an attacker model and see what happens.
-- where is the code you want to fault ? You need to select one or multiple intervals of adresses that will be faulted to fill the `target-addresses` option.
+- where is the code you want to fault ? You need to select one or multiple intervals of addresses that will be faulted to fill the `target-addresses` option. We recommend to have one injection target interval per function and omit the beginning pushing the return value on the stack. 
 - what fault model to use ? What type of faults to inject, how many at most ? 
-You can also ask to fault flags (which are not faulted by default), or to fault values serving as adresses (which are not by default as support for faults on adresses is not efficient, making the solver or the SE explodes).
+You can also ask to fault flags (which are not faulted by default), or to fault values serving as addresses (which are not by default as support for faults on addresses is not efficient, making the solver or the SE explodes).
 You can chose whether to have fault checks (number of fault lesser or equal to the maximum allowed, and fault constraints satisfied) at each fault location (good for branching models), at each branch (good for forkless models), or at the end.
 - you can set whether to stop the exploration at the first attack found, or explore everything.
 
 Then, start by adding one fault, and manually verify each result against assembly and C code to make sure the attacks found make sense. A bad configuration, especially an issue with initialization will yield incoherent results. Also, manually check all dynamic jumps that appear, you may have set the injection target to wide, or use a mode confusing the SE engine. Ideally, no dynamic jumps should be left.
 
-You may have to cut path exploration beyond a certain adresse, in error handling in particular, which is to add in the configuration as `directives`.
+You may have to cut path exploration beyond a certain address, in error handling in particular, which is to add in the configuration as `directives`.
 
 If you still have incorrect results, you can glimpse into BINSEC/ASE inner workings by displaying internal logs. The level goes from 0 (none) to 10 (everything). This is a `[sse]` option and can be written in the configuration file, but we found it easier to add it to the command line and to pipe the result in a file for examination as it can be very long depending on the level.
 ```
 binsec -config config.cfg -sse-debug-level 3 > log.txt
 ```
-
+Also, do not hesitate to open an issue or contact the authors.
 
 # Experiments
 

docs/performance_runs.md

@@ -9,7 +9,7 @@ Python scripts are in the `multirun-script` folder. The main script is `mutlirun
 
 It will output the logs produced by BINSEC/ASE and a csv file summing up essential metrics.
 
-***WARNING*** multirun.py is to be launched form the `multirun-script` folder for correct paths.
+***WARNING*** multirun.py is to be launched from the `multirun-script` folder for correct paths.
 ```
 cd /home/binsec-ase/artefact/multirun-script
 ```

getting_started.md

@@ -7,8 +7,6 @@ This artefact is available as a Docker or VM for VirtualBox.
 
 ## VM installation
 
-Download the [BINSEC/ASE VM](https://github.com/binsec/esop2023_artefact/releases/download/1.0/esop2023_artefact.ova).
-
 Import the `BINSEC-ASE` VM in VirtualBox. Start it.
 The user is `binsec-ase`, and the password `binsec-ase` though it should login automatically.
 
@@ -29,9 +27,10 @@ See the [step-by-step](./step_by_step.md) guide for further documentation.
 
 Download the [BINSEC/ASE docker](https://github.com/binsec/esop2023_artefact/releases/download/1.0/esop2023_artefact.tar.gz).
 
-Launch the docker with:
+Decompress and load the docker with the `load` command and launch it with:
 ```
-docker run -it --rm esop2023_artefact
+docker load < esop2023_artefact.tar.gz
+docker run -it esop2023_artefact
 ```
 Note that if you are using vscode, you can bind it to the docker.
 
@@ -42,6 +41,8 @@ cd /home/binsec-ase/artefact
 
 Note that some useful software are in `/home/binsec-ase/programs`, namely the solvers bitwuzla and boolector (z3 is also installed), the dissasembler cutter (radare2 is also installed).
 
+We refer the reader to the [docker manual](https://docs.docker.com/storage/volumes/) regarding volumes for persisting data generated by and used by the docker container.
+
 See the [step-by-step](./step_by_step.md) guide for further documentation.
 
 # Paper