project-oak
Parameterize AES proof over s-box
The AES s-box can be implemented in a wide variety of ways, with different timing properties and side-channel resistances. However, all of these implementations can easily be tested exhaustively, because the s-box has only 256 cases. Therefore, it seems to me that it's low-hanging fruit to write our AES proofs in such a way that any s-box implementation can be plugged in. We can still provide an end-to-end proof that plugs in the LUT or Canright s-box, but that proof would be just a specialization of one that can take any s-box.
Some of the s-box implementations take multiple cycles, so this would involve changing the cipher implementation to accept subroutines -- at least sub_bytes -- as Circuits instead of purely combinational components. Likewise, sub_bytes would need to allow a multi-cycle s-box.
We're prioritizing HMAC development instead, so I'm downgrading the priority of this change.