Add tutorials.

Fixes #2.

_config.yml

@@ -3,6 +3,9 @@ collections:
   tools:
     output: true
     permalink: /:collection/:name
+  tutorials:
+    output: true
+    permalink: /:collection/:name
 defaults:
  - scope:
      path: ""
@@ -13,3 +16,8 @@ defaults:
      type: "tools"
    values:
      layout: "tools"
+ - scope:
+     path: ""
+     type: "tutorials"
+   values:
+     layout: "tutorials"

_includes/tool_meta.html

@@ -0,0 +1,29 @@
+<div id="tool-metadata">
+	<table>
+		<colgroup>
+			<col>
+			<col>
+		</colgroup>
+		<tr><th scope="row">Year</th><td>{{ include.tool.year }}</td></tr>
+		<tr><th scope="row">Target</th><td>{{ include.tool.target }}</td></tr>
+		<tr><th scope="row">Technique</th><td>{{ include.tool.technique }}</td></tr>
+		<tr><th scope="row">Guarantees</th><td>{{ include.tool.guarantees }}</td></tr>
+		<tr><th scope="row">Available</th><td>{% if include.tool.available %}<b style="color: green;">yes</b>{% else %}<b style="color: red;">no</b>{% endif %}</td></tr>
+		{% if include.tool.repo %}<tr><th scope="row">Repository</th><td><a href="{{ include.tool.repo }}">{{ include.tool.repo }}</a></td></tr>{% endif %}
+		{% if include.tool.site %}<tr><th scope="row">Website</th><td><a href="{{ include.tool.site }}">{{ include.tool.site }}</a></td></tr>{% endif %}
+		{% if include.tool.papers %}
+		{% for paper in include.tool.papers %}
+		<tr><th scope="row">Paper<sub>{{ forloop.index }}</sub></th><td><a href="{{ paper.link }}">{{ paper.name }}</a></td></tr>
+		{% endfor %}
+		{% endif %}
+		{% if include.tutorials and include.tutorials.size > 0 %}
+		<tr><th scope="row">Tutorial</th><td><a href="{{ include.tutorials[0].url | relative_url }}"><b>yes</b></a></td></tr>
+		{% endif %}
+	</table>
+	<div id="tool-links">
+		<a href="{{ include.tool.url | relative_url }}"><button {% if include.which == "tool" %}class="inactive"{% endif %}>Tool page</button></a>
+		{% if include.tutorials and include.tutorials.size > 0 %}
+		<a href="{{ include.tutorials[0].url | relative_url }}"><button {% if include.which == "tutorial" %}class="inactive"{% endif %}>Tutorial page</button></a>
+		{% endif %}
+	</div>
+</div>

_layouts/tools.html

@@ -2,27 +2,11 @@
 layout: default
 ---
 
+{% assign tutorials = site.tutorials | where: "title", page.title %}
+{% assign tool = page %}
+
 <h2>Metadata</h2>
-<div id="tool-metadata">
-	<table>
-		<colgroup>
-			<col>
-			<col>
-		</colgroup>
-		<tr><th scope="row">Year</th><td>{{ page.year }}</td></tr>
-		<tr><th scope="row">Target</th><td>{{ page.target }}</td></tr>
-		<tr><th scope="row">Technique</th><td>{{ page.technique }}</td></tr>
-		<tr><th scope="row">Guarantees</th><td>{{ page.guarantees }}</td></tr>
-		<tr><th scope="row">Available</th><td>{% if page.available %}<b style="color: green;">yes</b>{% else %}<b style="color: red;">no</b>{% endif %}</td></tr>
-		{% if page.repo %}<tr><th scope="row">Repository</th><td><a href="{{ page.repo }}">{{ page.repo }}</a></td></tr>{% endif %}
-		{% if page.site %}<tr><th scope="row">Website</th><td><a href="{{ page.site }}">{{ page.site }}</a></td></tr>{% endif %}
-		{% if page.papers %}
-		{% for paper in page.papers %}
-		<tr><th scope="row">Paper<sub>{{ forloop.index }}</sub></th><td><a href="{{ paper.link }}">{{ paper.name }}</a></td></tr>
-		{% endfor %}
-		{% endif %}
-	</table>
-</div>
+{% include tool_meta.html tool=tool tutorials=tutorials which="tool" %}
 
 {{ content }}
 

_layouts/tutorials.html

@@ -0,0 +1,15 @@
+---
+layout: default
+---
+
+{% assign tutorials = page | sort %}
+{% assign tool = site.tools | where: "title", page.title | first %}
+
+<h2>Metadata</h2>
+{% include tool_meta.html tool=tool tutorials=tutorials which="tutorial" %}
+
+{{ content }}
+
+<hr/>
+Back to the <a href="{{ tool.url | relative_url }}"><b>Tool page</b></a>.
+

_tutorials/Binsec.md

@@ -0,0 +1,7 @@
+---
+slug: binsec
+title: Binsec
+description: "Constant Time Analysis with Binsec"
+---
+
+See the tutorial provided by [Binsec](https://github.com/binsec/binsec/blob/master/doc/sse/relse.md).

_tutorials/ct-verif.md

@@ -0,0 +1,66 @@
+---
+slug: ct-verif
+title: ct-verif
+description: "Constant Time Analysis with ct-verif"
+---
+
+Installation
+------------
+
+TODO.
+
+Markup (declaring secrets)
+--------------------------
+
+ct-verif enables you to declare the private and public variables and/or memory regions (arrays) containing secret or public inputs, declassified outputs, but also you need to declare those regions to be non-overlapping.
+ct-verif will pick up those secrets and look for influences on program behaviour violating the constant-time criterion (i.e. there shall be neither secret content dependent branching behaviour nor secret dependent memory address indexing (array accesses)).
+
+ct-verif expects a wrapper function containing a call to the function(s) you want to analyze. If you want to mark secret variables or memory areas, you need to do this using special markup declarations and compile a binary from this. You can include external libraries just like with any other C program and you can analyze those libraries, if you wish. First, let's look at the markup.
+
+You need to include the header file `ctverif.h` in your file, so you get to use them.
+The syntax for the markup declarations can be seen in `ctverif.h`, but will be succinctly shown here for your benefit. Some examples would be:
+```c
+void public_in(smack_value_t);
+void public_out(smack_value_t);
+void declassified_out(smack_value_t);
+void public_invariant(smack_value_t);
+```
+The only parameter of those functions is the name of your variable. You need to wrap your variable in a call to `__SMACK_value()`.
+The more complicated part is non-overlapping region markup:
+```c
+__disjoint_regions(addr1,len1,addr2,len2);
+```
+
+You can use it all in a practical example, taken from the official repository, like this:
+```c
+int curve25519_donna_wrapper(u8 *mypublic, const u8 *secret, const u8 *basepoint) {
+  __disjoint_regions(mypublic,32,secret,32);
+  __disjoint_regions(basepoint,32,secret,32);
+
+  /* Boilerplate (until modularity) */
+  public_in(__SMACK_value(mypublic));
+  public_in(__SMACK_value(secret));
+  public_in(__SMACK_value(basepoint));
+
+  /* Important stuff */
+  public_in(__SMACK_values(basepoint,32));
+  declassified_out(__SMACK_values(mypublic,32));
+  //  declassified_out_object(__SMACK_return_object());
+
+  return curve25519_donna(mypublic,secret,basepoint);
+}
+```
+
+For the full documentation, please refer to the ct-verif paper and the header files themselves.
+
+Analysis (compiling examples and running ct-verif)
+--------------------------------------------
+
+Using ct-verif compiles and analyzes programs in one step. After you have done the markup, you are ready to run ct-verif.
+
+You can run ct-verif on a source code file called `my_example.c` and analyze the code entry point `main` with the following command:
+```sh
+$ ctverif --entry-points main my_example.c
+```
+
+You can expect some warnings and a lot of debug output during compilation steps.

_tutorials/dudect.md

@@ -0,0 +1,88 @@
+---
+slug: dudect
+title: dudect
+description: "Constant Time Analysis with dudect"
+---
+
+Installation
+------------
+
+TODO.
+
+
+Preliminary work (setup dudect)
+-------------------------------
+
+dudect tries to detect if a specific operation executes in constant time. To do so, it evaluates the overall execution time of the function, feed with different inputs (we will talk about input *classes*), and check if the timing distribution are statistically different. Note that the target of the evaluation is considered as a black-box, so a different control flow resulting on the same exact execution time would not be detected. 
+
+Due to this black-box testing, there is no need to annotate the code. However, dudect expects a main() function in charge of setting the analysis parameters and running the analysis (with `dudect_main()`), and two functions to initialize the input classes and call the code to asses respectively. The file containing these declarations must include dudect.h as it contains all the code to perform the analysis.
+
+Two settings are available in the `dudect_config_t` structure:
+* `chunk_size`: size (in byte) of each piece of data to feed in as input, 
+* `number_measurements`: number of test to run before generating new inputs.
+
+The two functions must have the following signatures:
+```c
+/**
+ * Generates inputs used during testing (can be random of carefully chosen). 
+ * Each input is c->chunk_size long, and can be associated with a class . 
+ * @param c is the configuration defined in the main function
+ * @param input_data is a c->chunk_size * c->number_measurements buffer
+ * @param classes is a c->number_measurements buffer
+ */
+void prepare_inputs(dudect_config_t *c, uint8_t *input_data, uint8_t *classes);
+/**
+ * Proper wrapper calling operation to asses **once**. The input is a buffer, 
+ * so you may need to parse it if you want to vary multiple input of the 
+ * operation you are evaluating. 
+ */
+uint8_t do_one_computation(uint8_t *data);
+```
+
+You can use it all in a practical example, taken from the official repository, as follows:
+
+```c
+/* Evaluates the targeted operation, with fixed base point, on data */
+uint8_t do_one_computation(uint8_t *data) {
+  uint8_t out[32] = {0};
+  uint8_t ret = 0;
+  const uint8_t basepoint[32] = {9};
+  curve25519_donna(out, data, basepoint);
+  /* to avoid optimization */
+  ret ^= out[0];
+  return ret;
+}
+
+/* Generates two input classes : 
+ *  class 0 inputs are only 00 bytes
+ *  class 1 inputs are random bytes 
+*/
+void prepare_inputs(dudect_config_t *c, uint8_t *input_data, uint8_t *classes) {
+  randombytes(input_data, c->number_measurements * c->chunk_size);
+  for (size_t i = 0; i < c->number_measurements; i++) {
+    classes[i] = randombit();
+    if (classes[i] == 0) {
+      memset(input_data + (size_t)i * c->chunk_size, 0x00, c->chunk_size);
+    } else {
+      // leave random
+    }
+  }
+}
+```
+
+For the full documentation, please refer to the dudect paper, its repository and the header file itself. Namely, the different practical examples may help.
+
+Analysis (compiling examples and running dudect)
+------------------------------------------------
+
+Once the C wrapper is ready, you need to compile all the binaries (tested function and dudect file) to run the analysis. If the function to test is in a library, you can simply link the library and include the appropriate header in your C file.
+
+As a practical example, taken from the official repository, if the function to test is defined in curve25519-donna.c, and your dudect file is dut_donna.c, you can compile it like this:
+```sh
+gcc curve25519-donna.c dut_donna.c -o dut_donna -lm
+```
+
+The detailed output can be cryptic (lots of statistical information), but a clear message is displayed at the end of the line.
+
+Depending on how much repetitions you set, and if you repeat the analysis until a leakage is found, it may take a while (namely if the implementation is constant time). If you have no result after 5 minutes, it suggests there is no leakage _for the input classes you defined_.
+

_tutorials/haybale-pitchfork.md

@@ -0,0 +1,119 @@
+---
+slug: haybale-pitchfork
+title: haybale-pitchfork
+description: "Constant Time Analysis with haybale-pitchfork"
+---
+
+pitchfork will handle variables as abstract data, either public or secret, and perform some symbolic analysis to unroll all possible execution paths, tainting all data depending on a secret along the way. If a secret variable is used in a branch or memory access, a warning is raised with the execution trace leading to the constant time violation.    
+pitchfork works with LLVM bitcode, and not directly on the binary.
+
+Installation
+------------
+
+TODO.
+
+Bitcode generation
+------------------
+First, you need to generate the bitcode (an intermediate representation, between source code and assembly) corresponding to the code to asses. However, you don't need to annotate the target code in any way. 
+
+You can generate the bitcode (\*.bc files) form a source file by compiling it with clang. Simply use the flags `-c -emit-llvm`. To make debugging easier, you may want to generate LLVM text-format files (\*.ll) using the flags `-S -emit-llvm`, and compile for debugging. For instance, compiling main.c into LLVM bitcode would result in the following commands:
+```bash
+clang -g -c -emit-llvm main.c -o main.bc
+clang -g -S -emit-llvm main.c -o main.ll
+```
+
+Once you got the bitcode generated, all the following operations happens in a Rust wrapper.
+
+Markup (declaring secrets)
+--------------------------
+
+pitchfork expects a Rust file with a `main()` function containing a project (your bitcode file(s)), some configurations (default configurations are available) and the entry point you want to use (the function name). The file must include the pitchfork crate :
+```rust
+use pitchfork::*;
+```
+
+You can then check whether the function is constant-time in all its inputs, or if it ever makes some constant-time violation by calling
+```rust
+pub fn check_for_ct_violation_in_inputs<'p>(
+    funcname: &'p str, 
+    project: &'p Project, 
+    config: Config<'p, Backend>, 
+    pitchfork_config: &PitchforkConfig
+) -> ConstantTimeResultForFunction<'p>
+```
+This comes down to considering all inputs as secret. For a more fine grained analysis, you may need to define an abstract definition of its signature, to make some inputs secret (`AbstractData::secret()`), and others public (`AbstractData::default()`). Then, you can call pitchfork with 
+```rust
+pub fn check_for_ct_violation<'p>(
+    funcname: &'p str, 
+    project: &'p Project, 
+    args: Option<Vec<AbstractData>>, // This is the abstract signature
+    sd: &StructDescriptions,        
+    config: Config<'p, Backend>, 
+    pitchfork_config: &PitchforkConfig
+) -> ConstantTimeResultForFunction<'p>
+```
+Both aforementioned function can be printed to return the result of the analysis.
+
+You can use it all in a practical example like this:
+
+```rust
+fn main() {
+    // Create the project from the path
+    let project = Project::from_bc_dir(&Path::new("bitcode_dir/"), "bc")
+        .unwrap_or_else(|e| panic!("Failed to create project: {}", e));
+    // Assuming only the second input is secret
+    let sig = Some(vec![
+            AbstractData::default(),
+            AbstractData::secret(),
+            AbstractData::default(),
+        ]);
+
+    let result = check_for_ct_violation(
+		"curve_donna", 
+		&project, 
+		sig,
+		&StructDescriptions::new(),
+		Config::default(), 
+        &PitchforkConfig::default());
+
+    println!("{}", result);
+}
+```
+
+More information on how to fix some values in the signature, deal with pointers or data structures are available on Github, illustrated with practical examples.
+
+Analysis (running pitchfork)
+----------------------------
+
+Once you have generated your bitcode and created the Rust file, you need to compile it, and link the pitchfork crate. To define such dependencies, Rust works with Cargo files which require a particular directory architecture. Namely, your Rust source code should be in a src/ folder. The following minimalist Cargo.toml file should then do the trick :
+
+```toml
+[package]
+name = "pitchfork_harness"
+version = "1.0.0"
+edition = "2018"
+
+
+[dependencies.pitchfork]
+package = "haybale-pitchfork"
+path = "[PITCHFORK FOLDERNAME]"
+features = ["llvm-10"]
+```
+
+You should then have the following folder architecture:
+```
+./Cargo.toml
+./src/
+    main.rs
+./bitcode_folder/
+    *.bc
+    *.ll
+```
+
+You can run pitchfork using 
+```sh
+cargo run 
+```
+
+Code with a large number of paths (recursive function calls, large loops, ...) can be long to process. If you do not get any result after 10 minutes, you may want to run the pitchfork on some less complex code.
+