2022-02-02 10:56:14 EST Patrick Hurley: What are the challenges codeveloping and verifying SW and HW
2022-02-02 10:57:25 EST Renato Levy: We have spoken before here in this Summit about a contract between hardware and software. Could we use these techniques to validate such contact?
2022-02-02 10:57:52 EST Olin Sibert: What kind of changes have you needed to make in Linux and other operating systems to make effective use of these hardware security architectures? Are there publications about that?
2022-02-02 10:58:32 EST Renato Levy: Also, the processor is just one part of the problem. How do we extend this to the whole hardware system?
2022-02-02 10:59:07 EST Todd Humiston: Jason Li•10:58 AM RISC-V SSITH on FPGA - which technology in particular?
2022-02-02 10:59:35 EST Todd Humiston: (Jason is backstage)
2022-02-02 11:00:23 EST Paul Ratazzi: I can think of some examples of security properties that might be difficult to formally verify if implemented only in software, but closer to trivial to verify when hardware/physical security is brought into the equation. Has there been a systematic exploration of this opportunity space?
2022-02-02 11:01:15 EST Laura Tinnel: Yes
2022-02-02 11:01:31 EST Sean Peisert: Yes, it's up
2022-02-02 11:05:21 EST Keith Rebello: @Renata perhaps we need a new program to address this 😉
2022-02-02 11:06:50 EST Keith Rebello: @Jason have a variety of different RISC-V architectures that run on FPGAs. Happy to discuss with you.
2022-02-02 11:09:57 EST Keith Rebello: @Paul I agree with you! I am not aware of this being explored mostly due to the stove piping I mentioned. I think there is real opportunity here.
2022-02-02 11:24:11 EST Todd Humiston: From Jason Li•11:23 AM Robert - will your compartmentlization be supported by seL4 partitions? Or, with CHERI is seL4 partitioning still needed for memory separation? Or that's a practical question - practitioners' design choice - what to use, how to use, and cost-benefit analysis.
2022-02-02 11:31:50 EST Lenny Elliott: all good
2022-02-02 11:59:22 EST Olin Sibert: Where does the sequential ISA cut off? For example, does it include page table updates of page-modified bits? How much larger do you expect the concurrency spec and proof effort to be?
2022-02-02 12:12:27 EST Renato Levy: would not that belong to teh compiler first?
2022-02-02 12:19:46 EST Valerio Senni: How processor diversity can help in keeping the system operations?
2022-02-02 12:26:11 EST Olin Sibert: Where does the inference of checks take place? Is it dynamic as CPU instructions are executed, static before a binary starts executing, something else?