Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Stack zeroization on main with proofs #631

Merged
merged 10 commits into from
Dec 5, 2023
Merged

Stack zeroization on main with proofs #631

merged 10 commits into from
Dec 5, 2023

Commits on Nov 20, 2023

  1. Set alignment padding apart 

    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>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    7fc85f0 View commit details
    Browse the repository at this point in the history

  2. Print both stk_max and total_stack 

    Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    dce7482 View commit details
    Browse the repository at this point in the history

  3. Strengthen the proof of linearization 

    At the end of a call, rsp is back at the same point.

Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    ef27718 View commit details
    Browse the repository at this point in the history

  4. Strengthen the proof of linearization 

    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>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    c2c006a View commit details
    Browse the repository at this point in the history

  5. Stack zeroization: code and proof 

    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>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    dfb1464 View commit details
    Browse the repository at this point in the history

  6. Stack zeroization for x86 

    Code and proof

Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    c58ef28 View commit details
    Browse the repository at this point in the history

  7. Stack zeroization for x86: add tests 

    Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    8f5931c View commit details
    Browse the repository at this point in the history

  8. Stack zeroization for ARM 

    Code and proof

Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    d451b64 View commit details
    Browse the repository at this point in the history

  9. Stack zeroization for ARM: add tests 

    Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    3236156 View commit details
    Browse the repository at this point in the history

  10. Add Changelog entry 

    Co-authored-by: Santiago Arranz Olmos <santiago.arranz1@gmail.com>
    @eponier @sarranz
    eponier and sarranz committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    836dcfe View commit details
    Browse the repository at this point in the history