diff --git a/_config.yml b/_config.yml index c35282e..56e7729 100644 --- a/_config.yml +++ b/_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" \ No newline at end of file diff --git a/_includes/tool_meta.html b/_includes/tool_meta.html new file mode 100644 index 0000000..93a0941 --- /dev/null +++ b/_includes/tool_meta.html @@ -0,0 +1,29 @@ +
+ + + + + + + + + + + {% if include.tool.repo %}{% endif %} + {% if include.tool.site %}{% endif %} + {% if include.tool.papers %} + {% for paper in include.tool.papers %} + + {% endfor %} + {% endif %} + {% if include.tutorials and include.tutorials.size > 0 %} + + {% endif %} +
Year{{ include.tool.year }}
Target{{ include.tool.target }}
Technique{{ include.tool.technique }}
Guarantees{{ include.tool.guarantees }}
Available{% if include.tool.available %}yes{% else %}no{% endif %}
Repository{{ include.tool.repo }}
Website{{ include.tool.site }}
Paper{{ forloop.index }}{{ paper.name }}
Tutorialyes
+ +
\ No newline at end of file diff --git a/_layouts/tools.html b/_layouts/tools.html index 4f2fe8a..f67be1c 100644 --- a/_layouts/tools.html +++ b/_layouts/tools.html @@ -2,27 +2,11 @@ layout: default --- +{% assign tutorials = site.tutorials | where: "title", page.title %} +{% assign tool = page %} +

Metadata

-
- - - - - - - - - - - {% if page.repo %}{% endif %} - {% if page.site %}{% endif %} - {% if page.papers %} - {% for paper in page.papers %} - - {% endfor %} - {% endif %} -
Year{{ page.year }}
Target{{ page.target }}
Technique{{ page.technique }}
Guarantees{{ page.guarantees }}
Available{% if page.available %}yes{% else %}no{% endif %}
Repository{{ page.repo }}
Website{{ page.site }}
Paper{{ forloop.index }}{{ paper.name }}
-
+{% include tool_meta.html tool=tool tutorials=tutorials which="tool" %} {{ content }} diff --git a/_layouts/tutorials.html b/_layouts/tutorials.html new file mode 100644 index 0000000..8cb76f5 --- /dev/null +++ b/_layouts/tutorials.html @@ -0,0 +1,15 @@ +--- +layout: default +--- + +{% assign tutorials = page | sort %} +{% assign tool = site.tools | where: "title", page.title | first %} + +

Metadata

+{% include tool_meta.html tool=tool tutorials=tutorials which="tutorial" %} + +{{ content }} + +
+Back to the Tool page. + diff --git a/_tutorials/Binsec.md b/_tutorials/Binsec.md new file mode 100644 index 0000000..ba4082f --- /dev/null +++ b/_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). \ No newline at end of file diff --git a/_tutorials/ct-verif.md b/_tutorials/ct-verif.md new file mode 100644 index 0000000..0f3fae4 --- /dev/null +++ b/_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. \ No newline at end of file diff --git a/_tutorials/dudect.md b/_tutorials/dudect.md new file mode 100644 index 0000000..16b99ce --- /dev/null +++ b/_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_. + diff --git a/_tutorials/haybale-pitchfork.md b/_tutorials/haybale-pitchfork.md new file mode 100644 index 0000000..6745c7c --- /dev/null +++ b/_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>, // 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. + diff --git a/_tutorials/memsan.md b/_tutorials/memsan.md new file mode 100644 index 0000000..ad2cd60 --- /dev/null +++ b/_tutorials/memsan.md @@ -0,0 +1,55 @@ +--- +slug: memsan +title: MemSan +description: "Constant Time Analysis with MemSan" +--- + +The idea is to use the MemorySanitiser module shipped with clang to dynamically analyse binaries, looking for constant-time violations. This particular module is originally designed to raise a warning when some uninitialised variable is used in a branch or to perform some memory access. In our context, the idea is to annotate the source code so that secret elements are *poisoned* and considered as uninitialised during the analysis. + +Installation +------------ + +TODO. + +Markup (declaring secrets) +-------------------------- + +MemSan enables you to declare the private variables and/or memory regions (arrays) containing secret (*poison*), and to declassify variables (*unpoison*) in some part of the code if needed. +You can include external libraries just like with any other C program and you can analyse those libraries, if you wish (enable debugging if you want clear results). + +Since you will execute the binary, you need to define a main() function, declare / poison the appropriate inputs, and call the function to evaluate. The file must include the header file sanitizer/msan_interface.h to be able to annotate secret variables. + +The syntax for the markup declarations can be seen in the header file, but will be succinctly shown here for your benefit. +```c +/* Make memory region fully uninitialized (size bytes starting at a). */ +void __msan_poison(const volatile void *a, size_t size); +/* Make memory region fully initialized (size bytes starting at a). */ +void __msan_unpoison(const volatile void *a, size_t size); +/* Make a null-terminated string fully initialized. */ +void __msan_unpoison_string(const volatile char *a); +/* Make first n parameters of the next function call fully initialized. */ +void __msan_unpoison_param(size_t n); +``` +None of these function change the content of the buffer. + +Note that a single call to the function is evaluated, using the values you provided, so you may need to provide different inputs to explore the code and detect a constant-time violation. + +For the full documentation, please refer to the Clang documentation. + +Analysis (running MemSan) +------------------------- + +You need to compile your binary before you can analyse it - libraries without annotations can also be analysed using a C wrapper calling a specific function with annotated inputs. + +For MemSan to be enable, you need to specify the correct option, and use clang as a compiler. We strongly advised to compile the targeted code with debug symbols. + +You can generate binaries for analysis like so: +```sh +$ clang -fsanitize=memory -g my_example.c -o my_example +``` + +The compilation option `-fsanitize-memory-track-origins` can help to track down the origin of the issue. To get meaningful stack traces in error messages add `-fno-omit-frame-pointer`, and disable inline assembly if needed. + +By default, MemSan will stop after the first error. You can change this behaviour with the option `-fsanitize-recover=all`. + +You can then run the binary called "my_example" and check the warning. The run should be fairly quick, but may generate lots of warnings on large and complex code. If so, you may want to check if some of them are independent of your annotations. diff --git a/_tutorials/timecop.md b/_tutorials/timecop.md new file mode 100644 index 0000000..95695ad --- /dev/null +++ b/_tutorials/timecop.md @@ -0,0 +1,53 @@ +--- +slug: timecop +title: Timecop +description: "Constant Time Analysis with Timecop" +--- + +Timecop uses Valgrind's memcheck module to dynamically analyse binary, looking for constant-time violations. This particular module is originally designed to raise a warning when some uninitialised variable is used in a branch or to perform some memory access. The idea behind Timecop is to annotate the source code so that the secret elements are *poisoned* and considered as uninitialised by valgrind. + +Installation +------------ + +TODO. + + +Markup (declaring secrets) +-------------------------- + + +Timecop enables you to declare the private variables and/or memory regions (arrays) containing secret (*poison*), and to declassify variables (*unpoison*) in some part of the code if needed. +You can include external libraries just like with any other C program and you can analyse those libraries, if you wish (enable debugging if you want clear results). + +Since you will execute the binary with valgrind, you need to define a `main()` function, declare / poison the appropriate inputs, and call the function to evaluate. The file must include the header file `poison.h` to be able to annotate secret variables. + +The syntax for the markup declarations can be seen in poison.h, but will be succinctly shown here for your benefit. +```c +poison(addr, len); +unpoison(addr, len); +``` +Those functions respectively mark as secret and unmark `len` bytes starting at `addr`. + + +Note that a single call to the function is evaluated, using the values you provided, so you may need to provide different inputs to explore the code and detect a constant-time violation. + +For the full documentation, and a practical example, please refer to the Timecop website. + +Analysis (running Timecop) +-------------------------- + +You need to compile your binary before you can analyse it - libraries without annotations can also be analysed using a C wrapper calling a specific function with annotated inputs. + +For valgrind to be able to output details on where the error occurred, we strongly advised to compile the targeted code with debug symbols. + +You can generate binaries for analysis with your C compiler like so: +```sh +$ clang -Wall -Wextra -g my_example.c -o my_example +``` + +You can then run Timecop on the binary called "my_example" by running valgrind: +```sh +valgrind --track-origins=yes ./my_example +``` + +The run should be fairly quick, but may generate lots of warnings. If so, you may want to check if some of them are independent of your annotations. diff --git a/assets/css/style.scss b/assets/css/style.scss new file mode 100644 index 0000000..a399840 --- /dev/null +++ b/assets/css/style.scss @@ -0,0 +1,30 @@ +--- +--- + +@import "{{ site.theme }}"; + + +#tool-links { + margin-top: 2em; margin-bottom: 2em; +} + +#tool-links button { + color: rgb(96, 108, 113); + padding: 0.75rem 1rem; + border-width: 1px; + border-style: solid; + border-radius: 0.3em; + transition: color 0.2s, background-color 0.2s, border-color 0.2s; +} + +#tool-links button:hover { + color: rgba(96, 108, 113, 0.7); + background-color:rgba(239, 239, 239, 0.7); + border-color: rgba(96, 108, 113, 0.7); +} + +#tool-links .inactive { + color: rgb(131, 138, 141); + background-color:rgba(239, 239, 239, 0.5); + border-color: rgba(96, 108, 113, 0.7); +} \ No newline at end of file diff --git a/index.md b/index.md index 88e4748..4ea1185 100644 --- a/index.md +++ b/index.md @@ -18,15 +18,18 @@ Each tool has its own page with more information and resources, sometimes **even Target Technique Guarantees + Tutorial {% assign tools = site.tools | sort_natural: "title" %} {% for tool in tools %} + {% assign tutorials = site.tutorials | where: "title", tool.title %} {{ tool.title }} {{ tool.year }} {{ tool.target }} {{ tool.technique }} {{ tool.guarantees }} + {% if tutorials and tutorials.size > 0 %}yes{% endif %} {% endfor %}