mirage / eqaf Goto Github PK

View Code? Open in Web Editor NEW

50.0 50.0 10.0 255 KB

Constant time equal function to avoid timing attacks in OCaml

License: MIT License

OCaml 95.45% C 4.29% Standard ML 0.17% Makefile 0.09%

eqaf's Introduction

Build Unikernels in OCaml

MirageOS is a library operating system that constructs secure, performant and resource-efficient unikernels.

About

MirageOS is a library operating system that constructs unikernels for secure, high-performance network applications across various cloud computing and mobile platforms. Developers can write code on a traditional OS such as Linux or macOS. They can then compile their code into a fully-standalone, specialised unikernel that runs under the Xen or KVM hypervisors and lightweight hypervisors like FreeBSD's BHyve, OpenBSD's VMM. These unikernels can deploy on public clouds, like Amazon's Elastic Compute Cloud and Google Compute Engine, or private deployments.

The most up-to-date documentation can be found at the homepage. The site is a self-hosted unikernel. Simpler skeleton applications are also available online. MirageOS unikernels repositories are also available here or there.

This repository

This repository contains the mirage command-line tool to create and deploy applications with MirageOS. This tool wraps the specialised configuration and build steps required to build MirageOS on all the supported targets.

Local install

You will need the following:

a working OCaml compiler (4.08.0 or higher).
the Opam source package manager (2.1.0 or higher).
an x86_64 or armel Linux host to compile Xen kernels, or FreeBSD, OpenBSD or MacOS X for the solo5 and userlevel versions.

Then run:

$ opam install mirage
$ mirage --version

This should display at least version 4.0.0.

Using `mirage`

There are multiple stages to using mirage:

write config.ml to describe the components of your applications;
call mirage configure to generate the necessary code and metadata;
optionally call make depends to install external dependencies and download Opam packages in the current dune workspace.
call dune build to build a unikernel.

You can find documentation, walkthroughs and tutorials over on the MirageOS website. The install instructions are a good place to begin!

eqaf's People

Contributors

Stargazers

Watchers

Forkers

craigfe hannesm smorimoto msgpo cfcs kit-ty-kate zineb-ada dra27 fantomebeignet

eqaf's Issues

Regression spotted in OCaml 4.11.0

It seems that the check tool works for OCaml 4.10.0 and 4.09.0 but it does not work for 4.11.0. The assembly generated is a bit different and I think, we have a possible regression.

OCaml 5.00 support

Currently eqaf’s tests fail with OCaml 5.00:

# /usr/bin/ld: clock/libclock_stubs.a(clock_stubs.o): in function `clock_linux_get_time_byte':
# /home/opam/.opam/5.00/.opam-switch/build/eqaf.0.8/_build/default/clock/clock_stubs.c:25: undefined reference to `copy_int64'
# collect2: error: ld returned 1 exit status
# File "caml_startup", line 1:
# Error: Error during linking (exit code 1)
# Command [17] exited with code 2:
# $ (cd _build/default && /home/opam/.opam/5.00/bin/ocamlopt.opt -w -40 -g -o test/test_branch.exe clock/clock.cmxa -I clock /home/opam/.opam/5.00/lib/ocaml/unix.cmxa -I /home/opam/.opam/5.00/lib/ocaml lib/eqaf.cmxa test/.test_branch.eobjs/native/dune__exe__Test_branch.cmx)

Use `bechamel`

Introspect the assembly generated by OCaml

Tests about time spend by our functions are fragile and don't scale well for our purposes. An other way to check if we execute in constant-time functions is to introspect assembly code as we do manually - to see jmp, GC call, etc.

So an introspection of the generated assembly code by ocaml should be interesting to see if into a simple model, functions needs exactly same ticks to be executed.

why in C?

is it for the constant time? for performance? wouldn't a pure OCaml implementation (see below) work in the same fashion?

let eqaf a b =
  let len = min (String.length a) (String.length b) in
  let res = ref 0 in
  let get_int idx s = int_of_char (String.get s idx) in
  for i = 0 to pred len do
    res := !res land ((get_int i a) lxor (get_int i b))
  done ;
  !res = 0

Fix tests when "special context of execution" is not provided

Just an issue to track this recurring issue better: ocaml/opam-repository#16212 (comment)

As I said, I'd be really happy to see this resolved. It would make our life 10x better.

Expose `select`

I think it might be useful to expose select functions like

  val one_if_not_zero : int -> int
  (** [one_if_not_zero n] is a constant-time version of [if n <> 0 then 1 else 0].
       This is functionally equivalent to [!!n] in the C programming language. *)

  val select_int : int -> int -> int
  (** [select_int choose_b   a   b] is [a] if [choose_b = 0] and [b] otherwise.
       The comparison is constant-time and it should not be possible for a
       measuring adversary to determine anything about
       the values of [choose_b], [a], or [b].
   *)

Implementation could look conceptually look like:

let [@inline] one_if_not_zero n =
  (* Is there a faster way to do this in OCaml?
     Essentially we are casting an integer to a bool,
     then casting back to integer. It feels like maybe the Stdlib
     should provide something like that?
  *)
  let minus_one_or_less = (n asr Sys.int_size) in
  let one_or_more = (-n) asr Sys.int_size in
  (minus_one_or_less lor one_or_more) land 1
  
let [@inline] select_int choose_b a b =
  let one_if_choose_b = one_if_not_zero choose_b in
  let one_if_choose_a = one_if_choose_b lxor 1 in (* 0 if choose_b *)
  (b * one_if_choose_b) lor (a * one_if_choose_a)

I believe we can refactor a bunch of our existing code to use these primitives if we added them to the library.

Code that prompted suggestion

Edit: It looks like more recent versions of OCaml provide at least Stdlib.Bool.to_int, which at least on Godbolt compiles to a branched version: https://ocaml.godbolt.org/z/kbygwA

Not sure why that crappy code gets emitted, I would have expected a branch-free implementation. Maybe something to ask a compiler hacker about...

pextq %rax, %rax, %rax ; collect set bits (incl. GC bit)
andq $2                ; only care about GC + first set bit (if any)

or at least

dec %0                      ; 0 if only GC bit was set 
test %rax, %rax             ; set ZF flag (because it's zero)
setnz %al                   ; put ZF in lowest bit
leaq 1(%rax, %rax, 1), %rax ; shift ZF by 1, add GC bit
; %rax is 1 (=0 + GC bit) or 3 (= 1<<1 + GC bit)

core_bench

Clearly not the best to be able to compile projects which depend on eqaf on windows (eg. ocaml-git).