2022-02-02 15:18:22 EST Todd Carpenter: Hey, never apologize for Lisp!
2022-02-02 15:18:28 EST Michael Joseph: LISP is classic!
2022-02-02 15:25:32 EST David Hardin: BTW, ACL2 supports loops now.
2022-02-02 15:31:35 EST David Hardin: We did go back to the AAMP7 proofs for the Turnstile high-assurance guard product.
2022-02-02 15:32:41 EST Darren Cofer: "I do not think that word means what you think it means."
2022-02-02 15:36:15 EST Nicholas Evancich: Scheme = where it is at vs LISP
2022-02-02 15:37:25 EST Stuart Card: Thus our focus here on _capability based_ secure/trusted boot.
2022-02-02 15:39:38 EST June Andronick: do you think explaining a formal theorem on a whiteboard is easier or not than showing it in a theorem prover?
2022-02-02 15:40:01 EST Valerio Senni: How do you see the trend of separation implemented at the HW level, like ARM Secure Architecture concept and its development from TrustZone to the current state?
2022-02-02 15:41:31 EST Todd Carpenter: Ray, for many of the examples given, they're driven by avionics (integrity availability) as well as crypto systems (confidentiality emphasis). When did those properties start to receive equal attention (if ever)?
2022-02-02 15:42:06 EST Jason Li: Isn't AAMP7 certified first, then formally verified later?
2022-02-02 15:42:50 EST Jason Li: Also, if I remember correctly, June/Gernot mentioned that as much as the proof is great, ultimately it's about the team who builds it, being kernel or a system.
2022-02-02 15:44:20 EST Todd Carpenter: Fantastic response and great examples Ray, Thanks!
2022-02-02 15:44:22 EST Gernot Heiser: the RISC-V CIA proofs were actually done at TS
2022-02-02 15:44:29 EST Stuart Card: We are struggling with the safety vs security issue in unmanned aircraft system remote identification.
2022-02-02 15:45:22 EST Nicholas Evancich: Ray, with the advent of MoonBounce, and the and the use of InsydeH20 as the framework most firmware is based on, do you think the next greenfield is apply "formal" to firmware creation?
2022-02-02 15:47:11 EST Raymond Richards: Nick,
2022-02-02 15:49:31 EST Raymond Richards: formal verification of microcode can be dicey. It is largely mnemonics of control setting for various pieces of the micro architecture. You end up tracking pipeline stages, and associated interactions. The AAMP7 had a short pipe (2 stages) and we only looked at the "kernel" which was 256 microaddresses. It still took a long time
2022-02-02 15:50:40 EST Raymond Richards: Other firmware may have issues with semantic specifications. YMMV
2022-02-02 15:51:16 EST Nicholas Evancich: Ray, thanks. I guess my real question is firmware keeps getting pushed into higher and higher level lang. So, maybe a good topic would be to tackle doing some formal on the rust version of this framework
2022-02-02 15:52:23 EST Raymond Richards: What would be the proof goals on firmware, proof of reaching a particular state?
2022-02-02 15:53:29 EST Axel Heider: Either this or proof your loader/updater/recovery works.
2022-02-02 15:53:31 EST Nicholas Evancich: Yeah, I'm thinking mostly boot and knowing that the CPU is in the "correct" state
2022-02-02 15:54:38 EST Nicholas Evancich: Then when microcode patches come out, maybe the BIOS / firmware can do some sanity checks
2022-02-02 15:56:34 EST Axel Heider: I think for patches that should be handled offline and the firmware trusts in a proper signature - which it has to check. An embedded system reasoning of patches seem a bit overkill an a low level.
2022-02-02 15:57:51 EST Nicholas Evancich: Sorry, I mean just on boot-up
2022-02-02 15:58:03 EST Raymond Richards: Both the AAMP7 and Green Hills proofs assumed a "correct initial state". The definition of which was capture in documents called embedment manuals and the onus is on the system developer to reach such a state.
2022-02-02 15:58:17 EST Axel Heider: What your chip might want to have it a recovery (A/B Partitions) that allows rolling back if the patches fail. Question is now how you conclude the update failed - classic watchdog comes to rescue?
2022-02-02 15:59:27 EST Nicholas Evancich: Ray, totally agree and it bugs me to no end that the manual for the correct state for intel is sitting in NorCal and we don't get it
2022-02-02 16:00:05 EST Nicholas Evancich: Axel, agreed. Or, you just exclude those asm that fail the verification
2022-02-02 16:00:38 EST Axel Heider: Concerning the formalization of the initial state I wondering if ARM's formalization of their architecture is something that comes handy here - I wonder if this has been explored somewhere
2022-02-02 16:06:32 EST Renato Levy: if we want trusted system popular: Eco System