Stack zeroization on main with proofs #631
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The padding introduced by the alignment at the start of the export function is no longer included in the frame size of the export function, only in the max stack size. And we distinguish two max stack sizes: - stk_max : the amount of stack without the padding. This is the amount of stack that the function may write to. - total_stack : this is the amount of stack including the padding. This is the minimal stack space required for the execution of the compiled program. This is the amount to use in the correctness theorem. Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
At the end of a call, rsp is back at the same point. Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
The fact that the memory that is not part of the source memory and not part of the stack is untouched is made explicit. This is needed to prove stack zeroization. Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
But just the generic part for the moment. The architecture-dependent parts (for x86 and ARM) are TODOs. Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
Code and proof Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
Code and proof Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
eponier
force-pushed
the
clear-stack_reborn
branch
from
cf4c897
to
3236156
Compare
|
ARM part done. The PR is ready! |
Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
eponier
force-pushed
the
clear-stack_reborn
branch
from
8b7dfb0
to
836dcfe
Compare
|
Great, I will try to read it soon. |
bgregoir
reviewed
Dec 1, 2023
| @@ -712,38 +857,63 @@ Lemma compile_prog_to_asmP | |||
| -> exists xm', | |||
| [/\ asmsem_exportcall xp fn xm xm' | |||
| , mem_agreement m' (asm_mem xm') (asm_rip xm') (asm_globs xp), asm_scs xm' = scs' | |||
| , (cparams.(stack_zero_info) fn <> None -> | |||
There was a problem hiding this comment.
I think this is not very nice to use cparams.(stack_zero_info) here.
Because there is no guaranties on its value.
I think we should add a boolean flag in the function (source level) and refers to it. So we will have the guaranty that if the source function is annotated then the stack is cleared.
|
I reviewed the statements (not proofs) of the lemmas in this PR and they look good to me. |
bgregoir
approved these changes
Dec 5, 2023
jedisct1
added a commit
to jedisct1/aegis-jasmin
that referenced
this pull request
Dec 5, 2023
Finally merged into Jasmin 🎉 jasmin-lang/jasmin#631
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is (finally...) stack zeroization on latest main with proofs. The code is the last version (the one that makes Valgrind happy). The separation in commits should be meaningful.
I tried to consistently rename every "clear stack" to "stack zero".
The arm part is missing for the moment, so I put the PR as a draft for now.