Due: Mon, 23 May 2016 23:00:00 -0700
Read RockSalt: Better, Faster, Stronger SFI for the x86, PLDI 2012.
Take a look at the git repo.
Which design decisions weaken the formal guarantees provided by RockSalt? Do you believe in the correctness of the C code that they hand translate?
What would need to be done to remove the C code from the TCB?
Jumps in RockSalt must be prefixed by a mask that ensures that the jump target is a multiple of 32. After executing the mask, but before executing the jump, the machine state is no longer locally safe because the program counter does not point to a verified instruction. How does RockSalt account for this case in their definition of safety?
Provide a list of questions you would like to discuss.