Skip to content

Full ISA non-interference stepper #22

Closed

Description

@RobinWebbers

We can symbolically evaluate the ISA through the Stepper module in the attached branch. There are two main things to do though:

  1. Attach it to an actual program.
    • This entails marking what is secret and public and doing a non-interference check.
    • We can start with a very toy program though!
    • Like binsec, we probably also need to check at every branch individually (as not to blow up the search space)?
    • Once a toy program works, we can think about loading from a bigger program.
  2. It's probably going to be slow, we might need some array folding at some point. Solving this in Grisette is hard however: we need a path condition in order to do fast resolution but the solver doesn't permit this. We can think about how to solve this if step 1 is working!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions