Crypto code review

[vkanne-msft]

What is a crypto code review. Like a normal code review, but more critical as it is on crypto code.

Review of idealizations and crypto specification:

Grep of authId:

• [x] AEAD_GCM.fst *
• [ ] ConnInvariant.fst
• [x] Content.fst *
• [ ] DataStream.fst *
• [ ] ENC.fst *
• [ ] Encode.fst *
• [x] LHAE.fst *
• [ ] LHAEPlain.fst *
• [ ] MAC.fst
• [ ] MasterSecret.fst
• [ ] Record.fst
• [ ] StAE.fst
• [ ] StatefulLHAE.fst
• [ ] StatefulPlain.fst *
• [x] StreamAE.fst *
• [x] StreamAE.fsti
• [ ] StreamDeltas.fst
• [ ] StreamPlain.fst
• [ ] Test.fst
• [ ] TLS.fst
• [ ] TLSInfo.fst *
• [ ] TLSOutline.fst
• files also using safeId.

A major part of the review will be the KeySchedule (https://github.com/mitls/mitls-fstar/issues/18).

[markulf]

A first step is to define a process for reviewing our code. We should eventually turn this into a wiki page.

• test the verification, by writing adversarial code, malicious interactions should result in typing errors
• write down cryptographic assumptions on paper
• when necessary do a paper proof

[markulf]

@vkanne-msft this is really more of a meta-issue or epic that should be split into separate tasks. For all code we write there should be some testing and review, especially for (idealized) crypto code.

Could you help with expertise on how best do do a code review using github features?

[markulf]

As we are developing an idealization style some relevant issues are discussed on the F* side, see https://github.com/FStarLang/FStar/issues/674

This was fixed.

[markulf]

The push on the record paper definitely helped our understanding of some modules. Ticked in the above list. Still lots of work to be done, on verification and review.

[vkanne-msft]

@markulf Should we move this to Milestone 2

[markulf]

Yes, for the complete review. We should carve out a task for those modules that we verify for Milestone 1. Mostly on the Record protocol.