[FEATURE] Trusted boot specs in CN

[podhrmic]

Summary

The SHAVE trusted boot code has Frama-C specs. Convert the specs to CN.

• [ ] specs are converted
• [ ] write down any issues you encountered with CN
• [x] write requirements for the trusted boot and the trusted boot workflow, such that they can be turned into specification
• [ ] review the requirements
• [ ] connect the requirements to the code level specs
• [ ] create an example hello world program with the trusted boot workflow
• [ ] review the existing SAW and Cryptol files, optionally replace the crypto with HACL*

[peterohanley]

This will require memcmp and memcpy support in CN which is supposed to be part of the VIP pointer provenance patches. Otherwise there is an issue with subtracting pointers (cast to uintptr_t) and CN doesn't allow calling arbitrary pointers as function pointers (worked around with a helper trusted function that just does that step).

[podhrmic]

Thanks for the update. So it looks like this will need to wait until the fixes you mention land. @thatplguy can we bump the associated CN issues in priority?

[thatplguy]

Thanks for the update. So it looks like this will need to wait until the fixes you mention land. @thatplguy can we bump the associated CN issues in priority?

I'll investigate – this is the CN ticket to watch. Are you completely blocked on porting the trusted boot component? Blocked on verifying properties of trusted boot? Or do you have a workaround but it will need to be fixed before we can claim that this component is fully ported and verified?

[podhrmic]

@thatplguy we will just work on other components in the meantime, and verify trusted boot later

[peterohanley]

Are you completely blocked on porting the trusted boot component? Blocked on verifying properties of trusted boot? Or do you have a workaround but it will need to be fixed before we can claim that this component is fully ported and verified?

I could specify much of what remains, but after taking out the actual boot (CN doesn't let you call a mysterious address, so the actual call is unverified) and memcpy/memcmp (as discussed -- I could try specifying against locally specified versions but I think CN needs the VIP patches to actually handle this) there isn't much left. It's essentially SHA(); boot(); and attestation is completely gone.

@thatplguy we will just work on other components in the meantime, and verify trusted boot later

:+1:

[thatplguy]

There are initial CN library models checked into main here: https://github.com/rems-project/cerberus/blob/ca7bc60f361fd277e3f1768c43d11726f29683d9/tests/cn_vip_testsuite/cn_lemmas.h#L111

The workaround for now is to include cn_lemmas.h and replace calls to memcpy/memcmp with _memcpy/_memcmp.

I've linked this ticket in the related CN issue for a full solution.

[podhrmic]

@peterohanley is still finding bugs in CN, filing tickets on the way and adding specs to the Trusted boot code

[podhrmic]

@peterohanley please open a draft PR with your code

[podhrmic]

Currently blocked on https://github.com/rems-project/cerberus/issues/541 and https://github.com/rems-project/cerberus/issues/567