2022-02-01 13:00:44 EST Todd Humiston: We will resume shortly....please stand by
2022-02-01 13:04:02 EST Raymond Richards: audio?
2022-02-01 13:04:36 EST Jerry Dussault: My audio is fine.
2022-02-01 13:27:03 EST June Andronick: I would just like to point out that if the code used is not the one from the seL4 repository, it cannot be called seL4 (https://sel4.systems/Foundation/Trademark/)
2022-02-01 13:28:24 EST Kyung Kwak: We understand the point and call it as a Secure Kernel
2022-02-01 13:28:47 EST Kyung Kwak: or ASK if we will
2022-02-01 13:31:43 EST Michael Joseph: Excellent and informative
2022-02-01 14:25:55 EST Danielle Stewart: Will you provide a link to your paper? I am interested in that.
2022-02-01 14:26:42 EST Danielle Stewart: Yep!
2022-02-01 14:26:45 EST Danielle Stewart: Thank you!
2022-02-01 14:26:57 EST Sean Peisert: This walk was terrific, thank you.
2022-02-01 14:26:59 EST Sean Peisert: It was recently pointed out to me that the Frama-C approach can often get to the point you're writing 30 lines of ACSL for every 10 lines of C, and so the reality is that writing in Coq from the outset and extracting to OCaml might make a lot more more sense. I wonder if you have any thoughts on this approach. I also wonder if you have thoughts about starting from Rust or SPARK/Ada rather than C.
2022-02-01 14:33:16 EST Philip Johnson-Freyd: Danielle, paper is here https://arxiv.org/abs/2009.06834
2022-02-01 14:33:48 EST Danielle Stewart: Thank you, Philip, I look forward to reading it. Will be in touch if I have questions!
2022-02-01 14:54:43 EST Jason Li: Thanks for the interesting talk, Greg.
2022-02-01 14:54:44 EST Danielle Stewart: You weren't! Great talk.
2022-02-01 14:54:48 EST Raymond Richards: we heard you, Greg!
2022-02-01 14:55:23 EST Jason Li: In terms of FM tools, do you expect to leverage all that may be suitable, or you have a subset of favorite tools, such as solver, or theorem prover?
2022-02-01 14:55:24 EST Michael Joseph: Excellent. thought provoking on optimized and on total costs.
2022-02-01 14:56:06 EST Danielle Stewart: Do you see pushback from developers during the incorporation of FM into your industry?
2022-02-01 14:56:34 EST Danielle Stewart: ^^ developers or management, for that matter
2022-02-01 14:56:44 EST Jason Li: Co-design is defintely the way to go. The threshold may be quite high.
2022-02-01 14:57:55 EST Olin Sibert: How realistic is it to estimate cost to attack the near-perfect systems we can (but rarely do) construct today using FM, separation kernels, strong crypto, etc.? How does one estimate the cost to discover a vulnerability like RowHammer?
2022-02-01 14:58:09 EST Raymond Richards: Do you worry about sustainability of FM tools? Many are the oESTomes of R&D programs, researchers like to move on to more research, they do not like to support tools.
2022-02-01 14:58:27 EST Jason Li: Yes - right on, Ray!