Let's DOIT: Add support for DOIT-instruction list in (S)CT checkers #736

J08nY · 2024-02-23T10:50:49Z

This PR will add support for ensuring that secret values only go into guaranteed constant-time instructions (Intel DOITM, ARM DIT).

Currently it does the following:

Adds a script for semi-automated extraction of the Intel DOIT/ARM DIT lists. This script checks, in the Intel case, whether the opcodes on the list cover all the instruction encodings of the mnemonic on the list.
Adds a CLI option -help-instructions to the compiler that is similar to the -help-instrinsics one but prints all of the instructions for the given architecture that Jasmin understands along with their expanded variants. This is necessary for the automated extraction of the DIT/DOIT instructions that Jasmin supports. Example of output:

VPSUB:VPSUBB
VPSUB:VPSUBD
VPSUB:VPSUBQ
VPSUB:VPSUBW

Adds a CLI option -doit to the jazzct tool that switches the CT checker list of constant-time instructions from "all but DIV/MOD" to "only those in the DOIT/DIT" lists. This CLI option also checks that the compiler pass selected is during or after lowering, because the mode otherwise does not make sense.

Which compiler pass to run with

It needs to be done at least after lowering, to have the instructions.

When run right after lowering, the CT checker can have false positives in case of lines like:
if (_LT(of, cf, sf, zf)) {
because it will consider all of the flags, even though the _LT operator only actually considers some.
If run after inline variable propagation this problem disappears, because the expression will be replaced with one that contains only the used flags.

J08nY · 2024-03-11T19:47:03Z

I have just now noticed #608, which reorganizes the (S)CT checkers and introduces some of the functionality that this PR duplicates, namely the "checkCTafter" CLI option. What is the plan with that PR @bgregoir? Will it get merged soon? Should this get rebased on top of it?

I plan to cleanup the commits in this PR and would like to know which branch to base it on.

bgregoir

I have not taken the time to read all of the PR.
But two small remarks:

Can you propagate the change also in SCT ?
Clearly the changelog needs to be updated.

bgregoir · 2024-03-14T22:55:11Z

Forgot about the first I was stupid, it is done

compiler/src/arch_full.ml

compiler/src/x86_arch_full.ml

bgregoir

For the option checkCTafter should we use it always when we want to do doit?

bgregoir · 2024-03-14T23:16:27Z

Thank a lot for this PR, I am globally impressed by what you did.
I have some small remarks but maybe I misunderstood some parts.
I think the best will be to discuss of it next week.

J08nY · 2024-03-15T07:34:22Z

For the option checkCTafter should we use it always when we want to do doit?

Yeah, it does not make sense to use -doit unless you are checking CT after lowering. And as discussed in the PR message, doing it after propagate is even better.

J08nY · 2024-03-15T13:44:28Z

I implemented changes based on the review:

There is a changelog now.
Added a check that gives the user an error if DOIT is run without specifying a (S)CT checking pass that is not after lowering.
Added is_doit_asm_extra that tests extra ops for being constructed out of DOIT instructions.
Made the DOIT lists to be explicit pattern matches and removed the _ -> false.

One thing that needs to be done (and I do not know how to do it) is to properly print the ARM instructions in the -help-instructions. The x86_64 variant of the code should be cleaned up as well. The intended format of the output is as I described in the PR description:

VPSUB:VPSUBB
VPSUB:VPSUBD
VPSUB:VPSUBQ
VPSUB:VPSUBW

J08nY · 2024-05-08T13:15:21Z

I rebased this branch on top of current main. That means that now the -doit option is added to the jazzct binary.

compiler/CCT/fail/strict.jazz

bgregoir · 2024-05-13T07:30:16Z

compiler/config/tests.config

@@ -15,6 +15,12 @@ bin    = ./scripts/check-cct
 okdirs = !CCT/success
 kodirs = !CCT/fail

+[test-CCT-DOIT]


Should we add also a SCT DOIT?

Sure, let me add that.

bgregoir · 2024-05-13T07:39:53Z

CHANGELOG.md

+  (when the `-doit` flag is used) check that secrets are only used with
+  guaranteed constant time instructions (DOIT for Intel, DIT for ARM). This option
+  only makes sense when done after the lowering compiler pass, which can be ensured
+  with the new `-after` option.


for -doit, did we have a default pass ?

What do you mean by a default pass? There are two ways I guess:

Passing the -doit option also sets the compiler pass to be after inline propagation. If someone also uses the -after option they get an error? Or maybe they get an error only if the pass is before lowering?

Passing the -doit option does nothing to the compiler pass set, it needs to be set using the -after option and that will check that the set pass is after lowering. This is currently implemented (and I like it more, but I am open to suggestions).

I was more in favor of the first one, with
the solution "Or maybe they get an error only if the pass is before lowering?". I think the user don't need
to know the name of the pass.

Ok, makes sense.

bgregoir

I have added some extra small comment. Excepted those I think we will be ok.

bgregoir · 2024-05-14T12:25:46Z

CHANGELOG.md

+  (when the `-doit` flag is used) check that secrets are only used with
+  guaranteed constant time instructions (DOIT for Intel, DIT for ARM). This option
+  only makes sense when done after the lowering compiler pass, which can be ensured
+  with the new `-after` option.


I was more in favor of the first one, with
the solution "Or maybe they get an error only if the pass is before lowering?". I think the user don't need
to know the name of the pass.

bgregoir · 2024-05-14T12:28:24Z

compiler/CCT/fail/H_L_L.jazz

@@ -1,8 +1,9 @@
-fn add_H_L_L(#secret reg u64 x, #public reg u64 ya) -> #public reg u64 {
+export fn add_H_L_L(#secret reg u64 x, #public reg u64 ya) -> #public reg u64 {


Can you explain why you have change all the tests.
What is the motivation of adding the export.

If they are not marked export they are not present at the later compiler passes where DOIT checking happens :)

Then those programs are not suited for testing the new functionality.

Well, AFAIK the export does not change anything about them with regards to the CT checking (the ordinary tests would have caught that) so I believe these can be reused for DOIT checking. They should be reused to see that unless specific non-DOIT instructions are used DOIT checking is the same as CT checking.

This brings me to a broader point that DOIT-specific tests should be added, which I will work on.

Did you manually inspect the error messages of the CT checker before and after your change to validate that they are still the same? Do you expect the reviewers of your PR to do this boring work?

I would expect the tests (and some understanding of what the export keyword does) to ensure that. Nevertheless I just manually checked and there is no change in the ordinary CT checker output.

compiler/CCT/fail/strict.jazz

bgregoir · 2024-05-14T12:45:27Z

compiler/src/ct_checker_forward.ml

@@ -172,7 +172,7 @@ let pp_kind fmt k =
  if k = Flexible then Format.fprintf fmt "#%s " (string_of_lvl_kind k)

 let pp_arg fmt (x, (k, lvl)) =
-  Format.fprintf fmt "%a%a %a" pp_kind k  Lvl.pp lvl (Printer.pp_var ~debug:false) x
+  Format.fprintf fmt "%a%a %a" pp_kind k  Lvl.pp lvl (Printer.pp_var ~debug:!Glob_options.debug) x


This seems to be not the correct fix.
Debug may print many other infos that are usually used
to debug the compiler.
For doit, I am agree that it is important to print the info
(it is done after lower spill), name clashes can occur. But either replace this by just a true or a boolean
depending on the pass.

I see, if this is set depending on the pass then the pass would need to be passed through to the checker. I think this will be quite cumbersome.

Indeed, fixing this is non trivial and mostly unrelated to this PR. Therefore please:

open an issue

drop this commit from this PR.

Done: #810.

…ons.

When it is run after lowering (where it neess to be done for the DOIT option), the variables have ids that distinguish them and those are important to see in debug output.

Adds a CCT-DOIT test group that contains the normal CCT tests in the success condition and the failure condition as well as DOIT-specific tests in the failure condition. The DOIT-specific tests use the two non-DOIT instructions ROL and XCHG. Reusing the CCT tests required making their main functions "export" to make sure they are kept at the later compiler passes where DOIT checking needs to be done.

vbgl · 2024-05-28T19:27:10Z

I’ve taken to PR #811 some changes from this PR. Notable changes are that for armv7, instructions LDR, STR, and MOVT have been marked as secure. The rationale for memory accesses is that the documentation explicitly mentions that timing may only depend on the address (which is generically handled by the checker otherwise) and not on the exchanged data. For MOVT, the guess is that this instruction is not listed as a secure instruction of armv8 because it is not an instruction of armv8 in the first place.

vbgl · 2024-05-28T19:30:42Z

I believe that all the tooling proposed in this PR, namely data extraction from manufacturer’s websites and data extraction from Jasmin, may be moved to a different repository (e.g., attached to a publication related this work).

vbgl · 2024-05-28T19:34:56Z

Future steps might be:

move the DOIT data into the instruction descriptors;
prove that pseudo-instructions that are marked DOIT are indeed implemented using DOIT instructions only;
implement an independent auditing tool to validate that instructions that are marked secure in the Jasmin implementation are indeed secure according to the manufacturer’s documentation.

vbgl · 2024-06-24T15:51:24Z

Now that PR #736 has been merged, I suggest to close this one.

J08nY mentioned this pull request Feb 27, 2024

Make libjade use DOIT instructions on secrets formosa-crypto/libjade#108

Merged

8 tasks

J08nY mentioned this pull request Mar 7, 2024

Declassify annotation lost after inlining. #746

Open

J08nY changed the title ~~Let's DOIT~~ Let's DOIT: Add support for DOIT-instruction list in (S)CT checkers Mar 11, 2024

J08nY mentioned this pull request Mar 11, 2024

Compiler pass "add array init" creates a lval with a dummy location #718

Closed

J08nY force-pushed the feat/doit branch 5 times, most recently from 5b897c7 to fbec7b1 Compare March 12, 2024 17:12

J08nY marked this pull request as ready for review March 12, 2024 17:22

vbgl mentioned this pull request Mar 13, 2024

Attach more precise meta-data to variables introduced at compile-time #753

Merged

bgregoir reviewed Mar 14, 2024

View reviewed changes

compiler/src/arch_full.ml Show resolved Hide resolved

bgregoir reviewed Mar 14, 2024

View reviewed changes

compiler/src/x86_arch_full.ml Show resolved Hide resolved

bgregoir reviewed Mar 14, 2024

View reviewed changes

J08nY force-pushed the feat/doit branch 5 times, most recently from 30fd559 to 7ac5e20 Compare March 15, 2024 13:35

J08nY mentioned this pull request Apr 22, 2024

Minor CLI and CT checker cleanups #786

Merged

J08nY force-pushed the feat/doit branch from 7ac5e20 to 47a8b6c Compare May 8, 2024 13:11

J08nY mentioned this pull request May 8, 2024

Use jazzct for (S)CT checking formosa-crypto/libjade#122

Open

sarranz mentioned this pull request May 11, 2024

Make SLH lowering the last pass before Stack Allocation #794

Merged

bgregoir reviewed May 13, 2024

View reviewed changes

bgregoir reviewed May 14, 2024

View reviewed changes

J08nY force-pushed the feat/doit branch from 5f4e79e to 47a8b6c Compare May 14, 2024 13:12

J08nY added 6 commits May 14, 2024 15:13

Add -help-instructions option that prints Jasmin-recognized instructi…

2e2ebd4

…ons.

Print CT checker debug with full variable names.

be8c87c

When it is run after lowering (where it neess to be done for the DOIT option), the variables have ids that distinguish them and those are important to see in debug output.

Add Intel/ARM DOIT instruction lists and automate their extraction.

8f7a288

Add CHANGELOG entry.

c51791d

Add DOIT option to jazzct.

8798577

Check compiler pass in jazzct with DOIT.

11cde9a

J08nY force-pushed the feat/doit branch from 47a8b6c to a7e041f Compare May 14, 2024 13:13

J08nY force-pushed the feat/doit branch from a7e041f to d37bd9b Compare May 14, 2024 14:14

vbgl marked this pull request as draft May 28, 2024 04:41

vbgl mentioned this pull request May 28, 2024

Add support for DOIT #811

Merged

vbgl closed this Jun 24, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Let's DOIT: Add support for DOIT-instruction list in (S)CT checkers #736

Let's DOIT: Add support for DOIT-instruction list in (S)CT checkers #736

J08nY commented Feb 23, 2024 •

edited

Loading

J08nY commented Mar 11, 2024 •

edited

Loading

bgregoir left a comment

bgregoir commented Mar 14, 2024

bgregoir left a comment

bgregoir commented Mar 14, 2024

J08nY commented Mar 15, 2024

J08nY commented Mar 15, 2024

J08nY commented May 8, 2024

bgregoir May 13, 2024

J08nY May 14, 2024

bgregoir May 13, 2024

J08nY May 14, 2024

bgregoir May 14, 2024

J08nY May 14, 2024

bgregoir left a comment

bgregoir May 14, 2024

bgregoir May 14, 2024

J08nY May 14, 2024

vbgl May 14, 2024

J08nY May 14, 2024

vbgl May 14, 2024

J08nY May 14, 2024

bgregoir May 14, 2024

J08nY May 14, 2024

vbgl May 15, 2024

vbgl May 28, 2024

vbgl commented May 28, 2024

vbgl commented May 28, 2024

vbgl commented May 28, 2024

vbgl commented Jun 24, 2024

		@@ -1,8 +1,9 @@
		fn add_H_L_L(#secret reg u64 x, #public reg u64 ya) -> #public reg u64 {
		export fn add_H_L_L(#secret reg u64 x, #public reg u64 ya) -> #public reg u64 {

Let's DOIT: Add support for DOIT-instruction list in (S)CT checkers #736

Let's DOIT: Add support for DOIT-instruction list in (S)CT checkers #736

Conversation

J08nY commented Feb 23, 2024 • edited Loading

Which compiler pass to run with

J08nY commented Mar 11, 2024 • edited Loading

bgregoir left a comment

Choose a reason for hiding this comment

bgregoir commented Mar 14, 2024

bgregoir left a comment

Choose a reason for hiding this comment

bgregoir commented Mar 14, 2024

J08nY commented Mar 15, 2024

J08nY commented Mar 15, 2024

J08nY commented May 8, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bgregoir left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vbgl commented May 28, 2024

vbgl commented May 28, 2024

vbgl commented May 28, 2024

vbgl commented Jun 24, 2024

J08nY commented Feb 23, 2024 •

edited

Loading

J08nY commented Mar 11, 2024 •

edited

Loading