Formal Methods & Verification

Download

verification@lists.tockos.org

January 2025

3 participants
2 discussions

Progress verifying the Tock timer using Verus
by Eric Mugnier 14 Jan '25

14 Jan '25

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

1 0

Was: [Core WG] Re: Formal verification in Tock
by Amit Levy 14 Jan '25

14 Jan '25

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

2 1