0.1.0 (add choice of the output to sample)

README.md

@@ -10,7 +10,8 @@
     4.  [Heuristic abbreviations](#heuristic-abbreviations)
 4.  [Experiments](#experiments)
 5.  [Synthesize all blocks from a execution trace](#synthesize-all-blocks-from-a-execution-trace)
-6.  [References](#references)
+6.  [Synthesize a specific output](#synthesize-a-specific-output)
+7.  [References](#references)
 
 
 # Requirements
@@ -50,15 +51,15 @@ $ eval $(opam env)
 
 Then you can install ocaml dependencies presented previously using `opam install <package-name>`.
 
-Finally, to install xyntia, execute:
+Finally, to install Xyntia, execute:
 ```
 $ make
 $ make install
 ```
 
 # Usage
 
-The help of xyntia is available through `xyntia -help`. In the following we will explain the two ways for using xyntia. 
+The help of Xyntia is available through `xyntia -help`. In the following we will explain the two ways for using Xyntia. 
 
 ## Synthesizing functions from fun.ml predefined functions
 
@@ -208,8 +209,8 @@ Datasets used in [1] can be found in the `./datasets` directory.
 To launch Xyntia over a dataset (e.g., B2) with a given timeout (e.g., 1s) execute the following commands:
 
 ```
-$ ./scripts/bench/sample.py --bench ./datasets/b2 --out <resdir>
-$ ./scripts/bench/bench.py --bench ./datasets/b2 --timeout 1 --out <resdir>
+$ python3 ./scripts/bench/sample.py --bench ./datasets/b2 --out <resdir>
+$ python3 ./scripts/bench/bench.py --bench ./datasets/b2 --timeout 1 --out <resdir>
 ```
 
 The option and their meanings can be found through the `--help` option.
@@ -231,6 +232,24 @@ $ cd examples/bin && make && cd -
 $ ./scripts/utils/all_from_trace.sh --outdir <resdir> --all -- ./examples/bin/add
 ```
 
+# Synthesize a specific output
+
+The previous section explained how to synthesize each output of each basic block. However, you may be interested in only one output of one basic block.
+We explain how to do it for the `add` function of `./examples/bin/add` and the `eax` output.
+
+First, you need to trace the code:
+```
+$ ./scripts/utils/all_from_trace.sh --outdir <resdir> --gdb -- ./examples/bin/add
+```
+
+Then you need to find the basic block of interest in `<resdir>/add/cfgs`. In our case, this is the file `<resdir>/add/cfgs/0x56556191.bin`. 
+Now you can sample the `eax` output and run Xyntia over it:
+
+```
+$ python3 ./scripts/utils/binsec/sample.py --bin <resdir>/add/cfgs/0x56556191.bin --reg_out eax --out 0x56556191_eax
+$ xyntia 0x56556191_eax/out_0.json
+```
+
 # References
 
 [1] Menguy, G., Bardin, S., Bonichon, R., & Lima, C. D. S. (2021, November). Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (pp. 2513-2525).

scripts/utils/binsec/sample.py

@@ -110,7 +110,8 @@ def __init__(self, mem, stores, basesize):
 
     def remove(self, memorywrite):
         for st in memorywrite.stores:
-            self.stores.remove(st)
+            if st in self.stores:
+                self.stores.remove(st)
 
     def getBaseName(self):
         return "memwrite_{}".format(self.index)
@@ -378,12 +379,14 @@ def random_sample(solv, index_sample, inputs, outputs):
     return res
 
 
-def main(binary, nsamples, outdir, bits=32):
+def main(binary, nsamples, reg_out, outdir, bits=32):
     formula = extract_smt_formula(binary)
     solv = Solver(formula, bits)
 
     inputs = solv.get_register_reads() + solv.get_memory_reads()
     outputs = solv.get_register_writes() + solv.get_memory_writes()
+    if reg_out != None:
+        outputs = [ o for o in outputs if reg_out in o.getName() ]
 
     res = { 
         output: {
@@ -414,6 +417,7 @@ def main(binary, nsamples, outdir, bits=32):
     parser.add_argument('--bin', required=True, type=str, help="binary to load")
     parser.add_argument('--arch', required=False, type=str, help="architecture: x86, x64 (default: x86)")
     parser.add_argument('--nsamples', required=False, type=int, help="number of samples (default = 100)")
+    parser.add_argument('--reg_out', required=False, type=str, help="output register to sample (if not set, samples all outputs)")
     parser.add_argument('--out', required=True, type=str, help="output directory")
     args = parser.parse_args()
 
@@ -426,4 +430,4 @@ def main(binary, nsamples, outdir, bits=32):
     ARCH = args.arch if args.arch != None else "x86"
     nsamples = args.nsamples if args.nsamples != None else 100
 
-    main(args.bin, nsamples, args.out)
+    main(args.bin, nsamples, args.reg_out, args.out)