search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Use the actual Hmac Cava2 device instead of placeholders #946

Closed fshaked closed 2 years ago

samuelgruetter commented 3 years ago

Oh that's cool to see that these definitions already exist! But now, the BIG question: Can we simulate this whole thing using vm_compute? That is, can you make the Goal at the end of RunSha256SoftwareOnCava.v go through?

https://github.com/project-oak/silveroak/blob/4b0268816f8e1e14f207a0b93cc5d2c94cdc2189/silveroak-opentitan/hmac/end2end/RunSha256SoftwareOnCava.v#L110-L114

(you might have to use the trace function to debug, and to adapt the amount of fuel in the exists n, and to adapt device.maxRespDelay, and then it still might not work, and debugging support is so bad that maybe it will be easier to just prove it correct than to waste too much time on debugging...)

samuelgruetter commented 2 years ago

@fshaked @blaxill what's the current status on the "can we simulate this with vm_compute" question? Does it work? Or do we believe that all the code is present, but also some bugs are present? Or is someone still working on some code that needs to be written/changed and you don't expect this simulation to work yet?

fshaked commented 2 years ago

@fshaked @blaxill what's the current status on the "can we simulate this with vm_compute" question? Does it work? Or do we believe that all the code is present, but also some bugs are present? Or is someone still working on some code that needs to be written/changed and you don't expect this simulation to work yet?

Last time I looked at it the mac device was not ready (didn't implement the sha256 only mode). I should try it again, now that it's implemented.

samuelgruetter commented 2 years ago

I tried whether we can simulate it using vm_compute, but it seems that the first time the Cava Hmac device is invoked, execution becomes very slow and consumes a lot of memory, ie the following expression blows up under vm_compute:

Definition test :=
  step hmac_top (reset_state hmac_top)
       (true, (0%N, (0%N, (2%N, (0%N,
         ((0x41110000 + 0x800)%N, (0%N, (42%N, (0%N, true)))))))), tt).

It's not quite clear to me what could cause this blowup, and at first sight I couldn't find anything obviously slow (such as, eg, 2^32 on nat).