[otbn, pre_sca] Roadmap for COCO-OTBN work

[abdullahvarici]

Description

With the PRs #17100 and #17211, COCO-ALMA framework is ported to the OTBN core. In this issue, we want to create a roadmap to use the framework with the OTBN core and list some points that we need to investigate. Following GDoc will have intermediate results and discussions.

• [x] Be sure the tool is working with the OTBN correctly. See expected leakage as a result.
• [x] Find out the source code which is causing leakage in bignum register file. (More information is on GDoc. If needed update the RTL and run the analysis again, compare results.
• [x] Run and see isw_and algorithm do not cause any leakage.
• [ ] Adapt the framework to use arithmetic masking. Read this paper for this reason.
• [x] Run the analysis with the ECC algorithm code snippets and verify formally the OTBN is secure.

[vogelpi]

Futher tasks that come to my mind:

• [x] Add cycle counter in testbench to easily inspect waves and associate those waves with tool output. The counter has to be reset with the start pulse being sent.
• [x] Feed URND/RND signals (actual data only, not the handshake) out such that we can place a volatile_random label on these inputs. This will become very relevant for analyzing code snippets using URND and RND.

[moidx]

Moving to cryptolib milestone as this enables development in pre-silicon stages.

[vogelpi]

@abdullahvarici , please update this issue to:

1. Reflect the progress over the last couple of months including references to relevant PRs.
2. Document what the current status is, also in terms of potential support for analyzing arithmetic masking.

Thanks!

[abdullahvarici]

Over the last couple of months:

• The work was started with porting COCO-ALMA framework to the OTBN core. Modifications are done on a branch of the COCO-ALMA fork. You can see here to understand how to use the framework with the OTBN core.
• When we were doing some initial tests to be sure the framework is working with the OTBN correctly, the tool reported a leakage caused by the integrity check of the bignum register file output and use the result of this check in control and data flow. We believed that it is necessary to stop propagation of the secret label propagation for this signal as we don't expect to see a failure of the integrity check in normal conditions. To provide that, we added --excluded-signals option to the framework. After that, we managed to see expected results when analyzing simple code snippets with the OTBN core.
• The tool also found a leakage when analyzing masked AND algorithm on OTBN. After further investigation we found out that blanking was necessary on the ALU bignum flag register. This is implemented in the PR#17503 and then verified with the tool.
• We added a cycle counter in testbench to easily inspect waves and associate those waves with tool output. And also we fed URND/RND signals out so that we can place a volatile_random label on these inputs. See PR#17289
• We analyzed boolean_to_arithmetic routine in ECC P256 Keygen algorithm. We were seeing a stable type of leakage. Then we found out this is caused by a redundant bit used in the algorithm. When we modified the routine to not the use that extra bit (so by using 320-bit instead of 321-bit originally), then the leakage disappeared. It was also discussed and decided that that extra bit cannot be used to retrieve secret data. Other than this, the tool found some other leakages. We investigated those and modified the algorithm so that it uses dummy instructions and also some boolean fresh masking: FIX.
• I've prepared and made a presentation about Formal Masking Verification for OTBN. It includes some background information and also our findings.
• Some short code snippets on OTBN are created and analyzed with the framework. OTBN Assembly Security Guide is created regarding to our findings.
• There is also a potential support for analyzing arithmetic masking. The tool developers may have developed some kind of support but this is not published yet. It would be good to contact them about this.

[jadephilipoom]

I think this is done? We've added the findings to the OTBN style guide: https://opentitan.org/book/doc/contributing/style_guides/otbn_style_guide.html?highlight=secure%20coding#secure-coding-for-cryptography

I created https://github.com/lowRISC/opentitan/issues/24056 to track making the existing code follow these rules, but I think that's separate from this issue about actually doing the work to find the rules, so it's probably safe to close this now. Please feel free to reopen if I'm wrong here.

[vogelpi]

This sounds good to me, thanks @jadephilipoom .