Hi, Thomas gave a pretty good overview (thanks).
The work on eChronos aims at providing a framework to reason about concurrent code, where for eChronos concurrency mainly comes from interrupts that can happen during OS execution. There also is a starting project aiming at modelling and verifying the "big-lock" multicore version of seL4 (described in [0]). This is still at its early stages, where the first step is to provide a formalisation on concurrent C code. [0] http://ssrg.nicta.com.au/publications/nictaabstracts/Peters_DEH_15.abstract.pml Cheers, June -- Dr June Andronick Senior Researcher, DATA61 (formerly NICTA), Sydney Conjoint Senior Lecturer, UNSW http://www.ssrg.nicta.com.au/people/?cn=June+Andronick On 4/12/2015 11:46 am, Thomas Sewell wrote: > Hello Gergely. > > Most of the existing seL4 verification work doesn't involve > concurrency. On a single core system, the kernel will never be running > concurrently with anything else. This can be extended to some > multiprocessor systems by wrapping the kernel in a spinlock or by > dividing the system into multiple clones. I think that Michael von > Tessin discusses these options in detail in his thesis[1] and starts > looking at the verification problem. > > To my knowledge noone has yet completed any verification of a > multiple-thread system on top of seL4, which will require concurrency > reasoning. Some initial steps have been taken: the integrity proof [2] > for instance is a necessary step toward allowing verification of one > task to ignore the existence of other tasks that lack the authority to > interfere. If dataflow security is a verification concern, the > information flow proof can be used to establish that the task is not > accidentally leaking secure information via the kernel. > > There's also a concurrency focused group at Data61 (NICTA that was) > which aims to eventually verify systems built on seL4 [4], but for the > moment they are focusing on simpler concurrent systems built on the > smaller eChronos kernel [5]. > > [1]: > http://ssrg.nicta.com.au/publications/nictaabstracts/vonTessin:phd.abstract.pml > > [2]: > http://ssrg.nicta.com.au/publications/nictaabstracts/Sewell_WGMAK_11.abstract.pml > > [3]: > http://ssrg.nicta.com.au/publications/nictaabstracts/Murray_MBGBSLGK_13.abstract.pml > > [4]: http://ssrg.nicta.com.au/projects/TS/overallproof.pml > > [5]: > http://ssrg.nicta.com.au/publications/nictaabstracts/Andronick_LM_15.abstract.pml > > I hope that helps. Others might know more. > > Cheers, > Thomas. > > On 03/12/15 22:40, Gergely Buday wrote: >> Hi there, >> >> what should I read if I want to understand the verification of >> concurrent programs related to the sel4 project? >> >> I have found >> >> https://ssrg.nicta.com.au/publications/papers/Daum-phd.pdf >> >> https://ssrg.nicta.com.au/publications/papers/Daum_DSW_08.pdf >> >> http://ssrg.nicta.com.au/projects/concurrency/ >> >> Are there others? >> >> Cheers >> >> - Gergely >> >> >> _______________________________________________ >> Devel mailing list >> [email protected] >> https://sel4.systems/lists/listinfo/devel > > > ------------------------------------------------------------------------ > > The information in this e-mail may be confidential and subject to > legal professional privilege and/or copyright. National ICT Australia > Limited accepts no liability for any damage caused by this email or > its attachments. > > > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
