Hi all, These are all very wonderful connection! Having said that, core@ is not an appropriate list for this thread (core@ is for core working group business and is not a public list). Instead, devel@ might have been a fine jumping off point and verification@lists.tockos.org (now CC'd instead of core@) is best! Go forth and prove stuff! -Amit Philip Levis <pal@cs.stanford.edu> writes:
Awesome, thanks for the introduction. Hi Deian!
I think David Dill’s motivation is that he wants to learn Verus and play with verifying things, and Tock is a useful target.
Ranjit and Deian, if you have a particular problem that you think is interesting/tractable but is very deep in your queue, that would be helpful. I’m meeting with David on Wednesday, I can ask if he’s looking to explore stuff and learn on his own or interested in syncing up.
Phil
On Jan 13, 2025, at 4:48 PM, Patrick Pannuto <ppannuto@ucsd.edu> wrote:
There's a somewhat established formal verification effort going on at UCSD led by +Jhala, Ranjit <mailto:rjhala@ucsd.edu> and +Deian Stefan <mailto:deian@ucsd.edu> with lead postdocs/students +Eric Mugnier <mailto:emugnier@ucsd.edu>, +Nico Lehmann <mailto:nlehmann@ucsd.edu> , +Evan Johnson <mailto:e5johnso@ucsd.edu> , +Vivien Rindisbacher <mailto:vrindisbacher@ucsd.edu> (none of whom are on the core team list I think, so CC'ing to thread here).
I believe they already have a verified MPU for Cortex-M and are working on PMP for RISC-V. That's in Flux I think. There's also a version of the kernel alarm/timer subsystem verified in Verus. I believe the other areas of focus are context switch code and DMA, but I'll leave status/details/etc up to the verification team.
There's also a #verification channel in the Tock slack that was created after the Verification breakout at TockWorld 7 where a bunch of these and other folks hang out—though it doesn't look to have had too much traffic lately.
The FV team here meets weekly on Fridays, might be useful to sync with them directly?
-Pat
On Mon, Jan 13, 2025 at 3:08 PM Philip Levis <pal@cs.stanford.edu <mailto:pal@cs.stanford.edu>> wrote: David Dill, Clark Barrett, and a student reached out to me about where formal verification could help Tock. David is very interested in formal verification and Rust. He’s been talking with the Verus team at MSR, who suggested that Tock might be a good application target for him.
I’m meeting with him later this week. Are there problems that jump out as aspects of Tock that would be especially valuable to formally verify?
Phil _______________________________________________ Core Working Group mailing list -- core@lists.tockos.org <mailto:core@lists.tockos.org> To unsubscribe send an email to core-leave@lists.tockos.org <mailto:core-leave@lists.tockos.org>
_______________________________________________ Core Working Group mailing list -- core@lists.tockos.org To unsubscribe send an email to core-leave@lists.tockos.org
Agreed — sorry, was just looking for recommendations in core. verification@ is much better. Phil
On Jan 14, 2025, at 11:19 AM, Amit Levy <amit@amitlevy.com> wrote:
Hi all,
These are all very wonderful connection! Having said that, core@ is not an appropriate list for this thread (core@ is for core working group business and is not a public list).
Instead, devel@ might have been a fine jumping off point and verification@lists.tockos.org (now CC'd instead of core@) is best!
Go forth and prove stuff!
-Amit
Philip Levis <pal@cs.stanford.edu> writes:
Awesome, thanks for the introduction. Hi Deian!
I think David Dill’s motivation is that he wants to learn Verus and play with verifying things, and Tock is a useful target.
Ranjit and Deian, if you have a particular problem that you think is interesting/tractable but is very deep in your queue, that would be helpful. I’m meeting with David on Wednesday, I can ask if he’s looking to explore stuff and learn on his own or interested in syncing up.
Phil
On Jan 13, 2025, at 4:48 PM, Patrick Pannuto <ppannuto@ucsd.edu> wrote:
There's a somewhat established formal verification effort going on at UCSD led by +Jhala, Ranjit <mailto:rjhala@ucsd.edu> and +Deian Stefan <mailto:deian@ucsd.edu> with lead postdocs/students +Eric Mugnier <mailto:emugnier@ucsd.edu>, +Nico Lehmann <mailto:nlehmann@ucsd.edu> , +Evan Johnson <mailto:e5johnso@ucsd.edu> , +Vivien Rindisbacher <mailto:vrindisbacher@ucsd.edu> (none of whom are on the core team list I think, so CC'ing to thread here).
I believe they already have a verified MPU for Cortex-M and are working on PMP for RISC-V. That's in Flux I think. There's also a version of the kernel alarm/timer subsystem verified in Verus. I believe the other areas of focus are context switch code and DMA, but I'll leave status/details/etc up to the verification team.
There's also a #verification channel in the Tock slack that was created after the Verification breakout at TockWorld 7 where a bunch of these and other folks hang out—though it doesn't look to have had too much traffic lately.
The FV team here meets weekly on Fridays, might be useful to sync with them directly?
-Pat
On Mon, Jan 13, 2025 at 3:08 PM Philip Levis <pal@cs.stanford.edu <mailto:pal@cs.stanford.edu>> wrote: David Dill, Clark Barrett, and a student reached out to me about where formal verification could help Tock. David is very interested in formal verification and Rust. He’s been talking with the Verus team at MSR, who suggested that Tock might be a good application target for him.
I’m meeting with him later this week. Are there problems that jump out as aspects of Tock that would be especially valuable to formally verify?
Phil _______________________________________________ Core Working Group mailing list -- core@lists.tockos.org <mailto:core@lists.tockos.org> To unsubscribe send an email to core-leave@lists.tockos.org <mailto:core-leave@lists.tockos.org>
_______________________________________________ Core Working Group mailing list -- core@lists.tockos.org To unsubscribe send an email to core-leave@lists.tockos.org
At this point, we (David Dill and Livia Sun) are looking for examples of real things to verify with Verus instead of standard benchmarks. In my past work as a formal verification researcher, I've found that this is a good way to find interesting new problems as well as guiding my research in a practical direction. Someone suggested Tock, so we talked to Phil to learn more. If we continue pursuing this, we'll talk to Ranjit's group and Eric directly. If anyone knows of more work we should know about, or has more thoughts, please let us know. I may not be monitoring this forum, so feel free to send email to "David.L.Dill@gmail.com" Thanks a lot, Dave
participants (3)
-
Amit Levy -
David Dill -
Philip Levis