[aes, kmac, sca] Repeat formal masking verification experiments prior to tapeout

[vogelpi]

@johannheyszl brought it up in today's SCA meeting that we need to repeat the formal masking verification experiments close to tapeout. We have been running these experiments in the past (as well as with FPGA measurements) but there is the risk that something is introduced into the the RTL which doesn't show on FPGA but only in the ASIC netlist.

Related to that, we should try to port he formal masking verification flow into the production environment.

estimate 64 remaining 2023-03-23 63

[vogelpi]

Triaged for aes, needed for M2.5 because the masking countermeasures are very important for TO.

[vogelpi]

Update: @arnonsha , @zi-v , @ballifatih , @johannheyszl and I have been discussing (internal notes here) how we can achieve this. We've agreed on the following procedure and sub tasks:

• [x] @vogelpi to share a how-to and a pre-synthesized netlist of the AES S-Box obtained from Yosys as well as tool prerequisites
• [ ] @zi-v to get the formal tool and requirements installed locally and to perform a dry run using the Yosys netlist
• [x] @vogelpi to contact formal tool authors and clarifying how exactly to add stdcell library information to the formal tool
• [x] @ballifatih to integrate the closed-source stdcell library information to a closed copy of the tool and perform a test run using a netlist generated from the closed-source flow
• [ ] @zi-v and @arnonsha to repeat the experiment using this closed tool version an AES S-Box netlist obtained from the real backend flow

After that, this pre-verified and synthesized AES S-Box will be loaded into the final netlist.

[moidx]

Planning to work on this post M2.5, but leaving as part of the milestone as is something that needs to be done with the netlist after we sign-off the block.

[GregAC]

@vogelpi @moidx is this actually needed for M2.5.2?

[johannheyszl]

@msfschaffner is talking to Nuvoton about running this for AES. @ballifatih has prepared the tooling.

[GregAC]

Good to know, do we intend to run this before M2.5.2 and/or want to make it running a requirements of M2.5.2 or is this more a best effort do it when we can?

[johannheyszl]

IMO the consensus is that we cannot make it a requirement and it is best effort for M2.5.3.

[GregAC]

Great, in that case I'll shift this to M2.5.3

[johngt]

Please note change of status and milestone movement @vogelpi

[vogelpi]

Thanks for the heads up @johngt . This sounds good to me.

@ballifatih has been working on this and there was some excellent progress. Do you maybe want to give an update here @ballifatih and @johannheyszl ?

[ballifatih]

Just to clarify the diff of the progress on AES S-box verification, @vogelpi had already verified AES S-box from RTL level (with yosys synthesis), so we had a good confidence that RTL does not have SCA violations. However, it was not clear whether AES S-box netlist produced by the commerical synthesis tool contains some SCA violations. I can think of two possible reasons for that:

1. The synthesis tool is doing some clever optimization which introduces some SCA violations,
2. because the techlib cells are rich and offer complex gate types, expressing S-box in terms of these gates may introduce a violation.

The main challenge that I dealt was that CocoAlma can only handle simple gate types such as 2-fan-in boolean gates, 2-input MUX and simple FFs. Therefore, one cannot directly input S-box netlist with techlib cells, as CocoAlma does not know how to formally evaluate the leakage behavior of these complex gates. We briefly assessed whether it would be possible to add custom cell definitions to CocoAlma, but we did not follow this route, because it requires significant amount of work on CocoAlma side.

Instead we have a rather dummy approach of breaking down complex cell types into a circuit of smaller gates supported by CocoAlma. We take the AES S-box netlist (with techlib cells) and produce its simplified equivalent netlist by replacing each cells with its circuit equivalent. The simplified netlist then is verified by CocoAlma.

We plan to repeat this with the actual S-box netlist synthesized with proper constrains (the one I used in this flow was not synthesized with real constrains that goes into production).

[msfschaffner]

@vogelpi @johannheyszl Moved to M3 due to security implications. Please let me know if it should be moved back to M4.

[andreaskurth]

Depends on PR #22844, which is under review. @vogelpi is running analyses on FPGA. Formal looks good. Once that PR is merged, he'll ping the PD team to get the final netlist, which he'll then run through the formal tool.

[vogelpi]

PR #22844 got now merged and I've reached out to the PD team to get the netlist ready. @ballifatih is also in the loop and will take care of the verification. Thanks @ballifatih !

[andreaskurth]

PD team is working on this. No significant changes to AES S-box since ES. Discussed in triage: continue to track this in M4

[vogelpi]

In the meantime, the synthesized AES S-Box has been extracted and successfully analyzed using @ballifatih 's flow. The synthesized netlist has been verified in transient mode and as expected, it has been found to be 1st-order secure.

What's left is to ensure that the formally verified S-Box netlist is instantiated in the design. On the open source side, all relevant work has been done and I am thus closing the issue.

Many thanks everybody for the good collaboration on this important task!

[cdgori]

Just want to second the great collaboration here. To have working flows that can both formally verify and experimentally analyze these S-Boxes is really excellent work, considering the state of things 3-4 years ago the team has done a lot.

(If any student is looking for potentially interesting work, the CocoAlma work described above by @ballifatih on 6/15/2023 to support complex cells might be interesting, as decomposing the complex cells to simpler cells should give the same analysis/results but actually seeing that it does is another matter. I can certainly imagine some constructions of complex gates that are less glitchy than their decomposed equivalents, but I think in theory it's also possible for a complex gate implementation to be more glitchy. I might be wrong about that, and that's what would need to be studied further. Regardless, we have the experimental checks showing that we don't have any such issue here.)