773e148 | Jay Bosamiya | 06 June 2019, 22:50:05 UTC | Fix confusing typo :P | 06 June 2019, 22:50:05 UTC |
61edaee | Jay Bosamiya | 06 June 2019, 22:45:06 UTC | Update [Vale.X64.QuickCodes] due to latest changes | 06 June 2019, 22:45:06 UTC |
fc4375c | Jay Bosamiya | 06 June 2019, 00:48:58 UTC | Update [Vale.X64.Decls] due to latest changes | 06 June 2019, 00:52:05 UTC |
2d17135 | Jay Bosamiya | 06 June 2019, 00:41:49 UTC | Update StateLemmas; For some reason [lemma_to_flags] doesn't work though. :/ | 06 June 2019, 00:41:49 UTC |
990bfa6 | Jay Bosamiya | 06 June 2019, 00:36:23 UTC | Update [State] using the new [Flags] module | 06 June 2019, 00:36:23 UTC |
d328e71 | Jay Bosamiya | 06 June 2019, 00:33:37 UTC | Introduce [Vale.X64.Flags] module; similar to [Vale.X64.Regs] | 06 June 2019, 00:33:37 UTC |
35a3d7e | Jay Bosamiya | 06 June 2019, 00:14:59 UTC | The machine state should store the flags as a [flags_t] | 06 June 2019, 00:14:59 UTC |
acc8d8e | Jay Bosamiya | 06 June 2019, 00:13:16 UTC | We want the value of a flag to be a [option bool] | 06 June 2019, 00:13:16 UTC |
8c7fa77 | Jay Bosamiya | 06 June 2019, 00:12:11 UTC | Introduce [flag] type to be a refinement on integers. Introduce aliases for carry and overflow flags. | 06 June 2019, 00:12:36 UTC |
a0d15c1 | Chris Hawblitzel | 05 June 2019, 20:08:04 UTC | Increase z3rlimit in Hacl.Spec.Poly1305.Equiv | 05 June 2019, 20:08:04 UTC |
a6d7e27 | Chris Hawblitzel | 05 June 2019, 17:58:05 UTC | Small z3rlimit changes for Z3 4.8.5 | 05 June 2019, 17:58:05 UTC |
820d22d | Jonathan Protzenko | 04 June 2019, 20:29:06 UTC | Eliminate duplicated terminology in favor of a single, arbitrary one | 04 June 2019, 20:29:06 UTC |
e7f36a9 | Jonathan Protzenko | 04 June 2019, 20:28:47 UTC | hints | 04 June 2019, 20:28:47 UTC |
660994b | Jonathan Protzenko | 04 June 2019, 00:33:38 UTC | Minor tweak | 04 June 2019, 00:33:38 UTC |
31133eb | Jonathan Protzenko | 03 June 2019, 22:43:24 UTC | Resume work on EverCrypt.Hash.Incremental, while waiting to work on CTR | 03 June 2019, 22:43:24 UTC |
f2706a7 | Jonathan Protzenko | 03 June 2019, 22:43:10 UTC | hints | 03 June 2019, 22:43:10 UTC |
d39021d | Jonathan Protzenko | 03 June 2019, 21:21:23 UTC | Merge remote-tracking branch 'origin/protz_fstar_loop' into protz_ctr | 03 June 2019, 21:21:23 UTC |
8e08993 | Chris Hawblitzel | 01 June 2019, 21:03:13 UTC | Merge branch 'fstar-master' into _vale_generic | 01 June 2019, 21:03:13 UTC |
86ec68e | Chris Hawblitzel | 01 June 2019, 21:02:27 UTC | Rename state to vale_state | 01 June 2019, 21:02:27 UTC |
133c7d5 | Jonathan Protzenko | 01 June 2019, 03:40:36 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 01 June 2019, 03:40:36 UTC |
a5229cd | Chris Hawblitzel | 01 June 2019, 01:40:36 UTC | Merge branch 'fstar-master' into _vale_generic | 01 June 2019, 01:40:36 UTC |
b90d477 | Chris Hawblitzel | 01 June 2019, 01:36:03 UTC | Merge machine_eval_ins operations (including taint operations) into single pass | 01 June 2019, 01:36:03 UTC |
fe2d4c7 | Jonathan Protzenko | 01 June 2019, 01:35:42 UTC | A more precise .depend invocation that will solve some broken builds but not all (see FStarLang/FStar#1657) | 01 June 2019, 01:35:42 UTC |
b4a200d | Jonathan Protzenko | 01 June 2019, 01:34:56 UTC | hints | 01 June 2019, 01:34:56 UTC |
898df2e | Jonathan Protzenko | 31 May 2019, 20:17:15 UTC | Fix UTF-8 that got botched during Vale's mass-renaming | 31 May 2019, 20:17:15 UTC |
ea2ecb6 | Jonathan Protzenko | 31 May 2019, 20:17:10 UTC | Disable benchmarking tests since i) failures to build or run them are not caught and ii) the cmake invocation fails under the conditions of the everest upgrade | 31 May 2019, 20:17:10 UTC |
dd4877b | Chris Hawblitzel | 31 May 2019, 18:35:43 UTC | Merge branch 'fstar-master' into _vale_generic | 31 May 2019, 18:35:43 UTC |
0398ba4 | Chris Hawblitzel | 31 May 2019, 18:33:58 UTC | Share common operand type between operand64 and operand128 | 31 May 2019, 18:33:58 UTC |
52ffdad | Aymeric Fromherz | 30 May 2019, 15:15:34 UTC | Merge branch 'fstar-master' into afromher_readme | 30 May 2019, 15:15:34 UTC |
1033e42 | Aymeric Fromherz | 29 May 2019, 20:34:19 UTC | README: Update list of verified algorithms | 30 May 2019, 15:15:00 UTC |
e516669 | Aymeric Fromherz | 29 May 2019, 20:28:25 UTC | README: Update list of algs supported | 30 May 2019, 15:15:00 UTC |
c1ca708 | Chris Hawblitzel | 30 May 2019, 13:51:12 UTC | Merge branch 'fstar-master' into _vale_generic | 30 May 2019, 13:51:12 UTC |
84a3c95 | Christoph M. Wintersteiger | 30 May 2019, 12:21:20 UTC | Made gnuplot optional for benchmark runs. | 30 May 2019, 12:21:20 UTC |
9e03cd9 | Chris Hawblitzel | 30 May 2019, 05:53:56 UTC | Remove Vale.Lib.Workarounds | 30 May 2019, 05:53:56 UTC |
9267a83 | Chris Hawblitzel | 30 May 2019, 00:18:42 UTC | Update to latest Vale version and switch to --use_two_phase_tc true | 30 May 2019, 00:18:42 UTC |
bf2f5f3 | Aymeric Fromherz | 29 May 2019, 20:34:19 UTC | README: Update list of verified algorithms | 29 May 2019, 20:34:19 UTC |
5dc2a04 | Aymeric Fromherz | 29 May 2019, 20:28:25 UTC | README: Update list of algs supported | 29 May 2019, 20:28:25 UTC |
5f823a9 | Christoph M. Wintersteiger | 29 May 2019, 15:49:33 UTC | Benchmarks build fix | 29 May 2019, 15:49:33 UTC |
2af50b3 | Christoph M. Wintersteiger | 29 May 2019, 14:23:17 UTC | Benchmark build fixes | 29 May 2019, 14:23:17 UTC |
7bd70bf | Christoph M. Wintersteiger | 28 May 2019, 14:50:56 UTC | Benchmark script tweaks | 28 May 2019, 14:51:04 UTC |
206b8d2 | Christoph M. Wintersteiger | 08 May 2019, 07:28:15 UTC | Fix benchmark CI makefile | 28 May 2019, 14:51:03 UTC |
28dc010 | Christoph M. Wintersteiger | 07 May 2019, 20:03:02 UTC | debug benchmarks in CI | 28 May 2019, 14:51:03 UTC |
fbb5ed9 | Christoph M. Wintersteiger | 07 May 2019, 17:50:46 UTC | Fix directory search paths for benchmarks | 28 May 2019, 14:51:02 UTC |
2276f2b | Christoph M. Wintersteiger | 07 May 2019, 14:33:41 UTC | Benchmark script fixes | 28 May 2019, 14:51:02 UTC |
5466b57 | Christoph M. Wintersteiger | 07 May 2019, 14:32:04 UTC | Try CMake 3.5 for benchmarks | 28 May 2019, 14:51:01 UTC |
f86de77 | Chris Hawblitzel | 25 May 2019, 13:10:54 UTC | Use allow_inversion even more in Leakage_Ins | 25 May 2019, 13:10:54 UTC |
086fa5f | Chris Hawblitzel | 25 May 2019, 00:28:26 UTC | Use allow_inversion in Leakage_Ins | 25 May 2019, 00:28:26 UTC |
60790c8 | Aymeric Fromherz | 23 May 2019, 22:02:08 UTC | Make cpuid constant time | 23 May 2019, 22:02:08 UTC |
18bbf23 | Aymeric Fromherz | 23 May 2019, 18:43:23 UTC | Fix OCaml extraction | 23 May 2019, 18:43:23 UTC |
6c4b104 | Aymeric Fromherz | 23 May 2019, 18:01:00 UTC | Return val for taint analysis | 23 May 2019, 18:01:00 UTC |
3642e32 | Aymeric Fromherz | 23 May 2019, 16:58:01 UTC | Taint analysis: Check that return value does not leak secrets | 23 May 2019, 16:58:01 UTC |
a7ffc19 | Aymeric Fromherz | 22 May 2019, 17:37:35 UTC | Merge branch 'fstar-master' into afromher_run_taint | 22 May 2019, 17:37:35 UTC |
88a34d8 | Aymeric Fromherz | 22 May 2019, 17:37:02 UTC | Taint analysis: Only Rsp and the args are now public. Everything passes the analysis | 22 May 2019, 17:37:02 UTC |
f254e30 | Aymeric Fromherz | 22 May 2019, 03:12:29 UTC | Secret stack instructions + Secret store/restore registers for gcm | 22 May 2019, 03:12:29 UTC |
83eef39 | Aymeric Fromherz | 21 May 2019, 23:15:43 UTC | Make xmm comparison constant time | 21 May 2019, 23:15:43 UTC |
a47f71e | Santiago Zanella-Beguelin | 21 May 2019, 20:50:53 UTC | Add a portable distribution that uses -mtune=generic instead of -march=native -mtune=native | 21 May 2019, 20:50:53 UTC |
4ec808c | Aymeric Fromherz | 21 May 2019, 20:43:55 UTC | Reenable taint analysis at extraction | 21 May 2019, 20:43:55 UTC |
e907c1f | Chris Hawblitzel | 19 May 2019, 13:11:22 UTC | Remove tab characters and trailing whitespace from files in vale directory | 19 May 2019, 13:11:22 UTC |
5f3f81d | Chris Hawblitzel | 18 May 2019, 23:58:09 UTC | Update hints | 18 May 2019, 23:58:09 UTC |
a0b9e04 | Chris Hawblitzel | 18 May 2019, 19:59:58 UTC | Merge branch 'fstar-master' into _vale_generic | 18 May 2019, 19:59:58 UTC |
f55b1f3 | Chris Hawblitzel | 18 May 2019, 19:00:44 UTC | Rename modules in vale directory | 18 May 2019, 19:00:44 UTC |
191a53c | Santiago Zanella-Beguelin | 16 May 2019, 16:32:52 UTC | Fix maximum length of ciphertext in Spec.AEAD.decrypt and state correctness lemma | 16 May 2019, 16:32:52 UTC |
f2c8b60 | Chris Hawblitzel | 16 May 2019, 03:08:25 UTC | Merge Taint_Semantics_s into Bytes_Semantics_s, remove Taint_Semantics_s module | 16 May 2019, 03:08:25 UTC |
ac19640 | Chris Hawblitzel | 15 May 2019, 23:17:37 UTC | Remove tainted_code and tainted_codes | 15 May 2019, 23:17:37 UTC |
954dc53 | Chris Hawblitzel | 15 May 2019, 22:43:38 UTC | Remove tainted_ocmp | 15 May 2019, 22:43:38 UTC |
dbeb034 | Chris Hawblitzel | 15 May 2019, 18:52:31 UTC | Move taint to operands, and remove tainted_ins | 15 May 2019, 18:52:31 UTC |
ebaa66c | Chris Hawblitzel | 14 May 2019, 22:58:15 UTC | Trace observations for both out and inout operands | 14 May 2019, 22:58:15 UTC |
5f5fc9d | Chris Hawblitzel | 14 May 2019, 17:16:48 UTC | Fix some Bytes_Semantics proofs | 14 May 2019, 17:16:48 UTC |
6c2afd3 | Chris Hawblitzel | 14 May 2019, 15:39:29 UTC | Merge branch 'fstar-master' into _vale_generic | 14 May 2019, 15:39:29 UTC |
e89539f | Chris Hawblitzel | 14 May 2019, 15:37:27 UTC | Merge state and taintState into single type, machine_state | 14 May 2019, 15:37:27 UTC |
81620b1 | Aymeric Fromherz | 14 May 2019, 00:59:33 UTC | Merge branch 'fstar-master' into afromher_big_aesgcm | 14 May 2019, 00:59:33 UTC |
0423092 | Aymeric Fromherz | 14 May 2019, 00:58:50 UTC | Remove aesgcm length restriction from evercrypt | 14 May 2019, 00:58:50 UTC |
d73eacf | Aymeric Fromherz | 14 May 2019, 00:43:52 UTC | Low* wrappers for relaxed aesgcm + hints | 14 May 2019, 00:43:52 UTC |
a7ade35 | Aymeric Fromherz | 14 May 2019, 00:24:23 UTC | Remove restriction on length for optimised gcmencrypt | 14 May 2019, 00:24:23 UTC |
373cc75 | Aymeric Fromherz | 13 May 2019, 23:44:46 UTC | Remove restriction on length for optimised gcmdecrypt | 13 May 2019, 23:44:46 UTC |
324069f | Aymeric Fromherz | 13 May 2019, 20:22:19 UTC | Fix decrypt + hints | 13 May 2019, 20:22:19 UTC |
8525f15 | Aymeric Fromherz | 13 May 2019, 18:03:38 UTC | Fix optimised aes-gcm | 13 May 2019, 18:03:38 UTC |
8265630 | Aymeric Fromherz | 13 May 2019, 17:47:26 UTC | WIP: Relax length requirement for gcmencrypt/decrypt | 13 May 2019, 17:47:26 UTC |
1be3f76 | Chris Hawblitzel | 12 May 2019, 16:53:34 UTC | Change x64 reg type from datatype to integer type | 12 May 2019, 16:53:34 UTC |
9101826 | Chris Hawblitzel | 10 May 2019, 20:34:05 UTC | Merge branch 'fstar-master' into _vale_leakage | 10 May 2019, 20:34:05 UTC |
cda4145 | Chris Hawblitzel | 10 May 2019, 19:34:29 UTC | Merge branch 'fstar-master' of https://github.com/project-everest/hacl-star into fstar-master | 10 May 2019, 19:34:29 UTC |
c9f3915 | Chris Hawblitzel | 10 May 2019, 19:32:15 UTC | In Makefile, make FSTAR_NO_FLAGS and PYTHON3 configurable | 10 May 2019, 19:32:15 UTC |
f247528 | Chris Hawblitzel | 10 May 2019, 18:02:31 UTC | Merge branch 'fstar-master' into _vale_leakage | 10 May 2019, 18:02:31 UTC |
cb75580 | Jonathan Protzenko | 10 May 2019, 16:50:54 UTC | More customizations for CCF | 10 May 2019, 16:50:54 UTC |
b04c00a | Santiago Zanella-Beguelin | 10 May 2019, 14:46:19 UTC | Hints | 10 May 2019, 14:46:19 UTC |
039f5de | Aymeric Fromherz | 10 May 2019, 14:27:09 UTC | Merge branch 'fstar-master' into afromher_big_aesgcm | 10 May 2019, 14:27:26 UTC |
f4a74d4 | Santiago Zanella-Beguelin | 10 May 2019, 12:35:24 UTC | Add function to free state in EverCrypt.Hash.Incremental | 10 May 2019, 12:35:24 UTC |
ca3e12f | Jonathan Protzenko | 09 May 2019, 19:01:18 UTC | Fix two assumes added at the interface between Ed25519 / SHA512 when the connection was made | 09 May 2019, 19:01:18 UTC |
a6b22a4 | Jonathan Protzenko | 09 May 2019, 19:01:02 UTC | Remove antediluvian code that became unreachable when we landed the WIP ed25519 | 09 May 2019, 19:01:02 UTC |
74a1f51 | Jonathan Protzenko | 08 May 2019, 14:51:31 UTC | hints | 08 May 2019, 14:51:31 UTC |
f0001a0 | Jonathan Protzenko | 08 May 2019, 14:49:22 UTC | temporary fix: z3refresh + a couple small changes to get this proof to go through | 08 May 2019, 14:49:22 UTC |
55dd80a | Jonathan Protzenko | 08 May 2019, 14:31:57 UTC | Some work on proof quality. rlimit 200 --> rlimit 50 + replayable hints | 08 May 2019, 14:31:57 UTC |
fdd1ea9 | Aymeric Fromherz | 08 May 2019, 03:54:13 UTC | Hints | 08 May 2019, 03:54:13 UTC |
e3eab20 | Aymeric Fromherz | 08 May 2019, 03:37:12 UTC | Merge branch '_vale_leakage' into _vale_leakage_stack | 08 May 2019, 03:37:12 UTC |
599a854 | Aymeric Fromherz | 08 May 2019, 02:59:40 UTC | StackTaint: Fix GCM{de,en}cryptOpt | 08 May 2019, 02:59:40 UTC |
69d7fa2 | Aymeric Fromherz | 08 May 2019, 01:24:33 UTC | Fix stackTaint interop | 08 May 2019, 01:24:33 UTC |
ad6adb3 | Aymeric Fromherz | 08 May 2019, 01:18:06 UTC | More refactoring for stack taint | 08 May 2019, 01:18:06 UTC |
d4f1bbf | Chris Hawblitzel | 07 May 2019, 21:33:57 UTC | Update Vale version to prepare for new F* version | 07 May 2019, 21:33:57 UTC |
df98277 | Aymeric Fromherz | 07 May 2019, 19:58:28 UTC | Taint analysis for stack instructions | 07 May 2019, 19:58:28 UTC |
31d74b5 | Jonathan Protzenko | 07 May 2019, 15:24:59 UTC | Merge pull request #159 from project-everest/taramana_tests Taramana tests | 07 May 2019, 15:24:59 UTC |