January 2025 - Formal Methods & Verification

Re: Was: [Core WG] Re: Formal verification in Tock

by David Dill

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(a)gmail.com" Thanks a lot, Dave

Jan. 16, 2025

Re: Progress verifying the Tock timer using Verus

by David Dill

Eric, Thanks for posting that report, and I'm pleased to meet you. I haven't used Verus except for simple examples, so it was enlightening to see how the limitations of the system posed problems for real code. David Dill

Jan. 16, 2025

Progress verifying the Tock timer using Verus

by Eric Mugnier

Hi all, I wanted to share an update on my progress verifying the Tock timer using Verus, with a report attached to this email. TL;DR: While the process has been challenging due to the effort required to adapt Tock code for the Verus verifier, there’s promising progress, and I’m optimistic about the outcome, although I lack time to work on it. Best, Eric Mugnier Ph.D. @ UCSD

Jan. 15, 2025

Re: Was: [Core WG] Re: Formal verification in Tock

by Philip Levis

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(a)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(a)lists.tockos.org (now CC'd instead of core@) is best! > > Go forth and prove stuff! > > -Amit > > Philip Levis <pal(a)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(a)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(a)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(a)lists.tockos.org <mailto:core@lists.tockos.org> >>> To unsubscribe send an email to core-leave(a)lists.tockos.org <mailto:core-leave@lists.tockos.org> >> >> _______________________________________________ >> Core Working Group mailing list -- core(a)lists.tockos.org >> To unsubscribe send an email to core-leave(a)lists.tockos.org

Jan. 14, 2025

Was: [Core WG] Re: Formal verification in Tock

by Amit Levy

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(a)lists.tockos.org (now CC'd instead of core@) is best! Go forth and prove stuff! -Amit Philip Levis <pal(a)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(a)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(a)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(a)lists.tockos.org <mailto:core@lists.tockos.org> >> To unsubscribe send an email to core-leave(a)lists.tockos.org <mailto:core-leave@lists.tockos.org> > > _______________________________________________ > Core Working Group mailing list -- core(a)lists.tockos.org > To unsubscribe send an email to core-leave(a)lists.tockos.org

Jan. 14, 2025