HolBA
HolBA copied to clipboard
kth-step
Binary analysis in HOL
It would be nice to prove the example using two different approaches: - composing contracts in BIR - composing contracts in ARM
The current HOLBA building and installation process requires many manual steps, such as installing a custom HOL4. This issue is about outlining and documenting possible improvements (automation) of building, installation,...
When generating weakest preconditions for programs containing many `BExp_Load`s and `BExp_Store`s - meaning any programs which uses the stack and not only purely registers - the multiple memory updates cause...
How do we compose contracts? - exec-to-label has composition problems - ?n exec-blocks is weaker and does not allow
We need this for debugging Scam-V (in particular, to inspect the generated stuff) without going insane. It's also nice for usability/user-interface reasons in case we find a counterexample and want...
Once an attacker/observation model is fixed, this should also determine the code we use to measure the channel on the hardware. So we would like to reflect this in the...
I open this issue to think about uploading posters and slides about HolBA somewhere in the wiki or docs folder.
The current Python wrapper doesn't handle memory expressions. I'm opening this issue to keep track of this :slightly_smiling_face: I wanted to use it to help me debug my WPs, but...