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.... [2]: http://ssrg.nicta.com.au/publications/nictaabstracts/Sewell_WGMAK_11.abstrac... [3]: http://ssrg.nicta.com.au/publications/nictaabstracts/Murray_MBGBSLGK_13.abst... [4]: http://ssrg.nicta.com.au/projects/TS/overallproof.pml [5]: http://ssrg.nicta.com.au/publications/nictaabstracts/Andronick_LM_15.abstrac... 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 Devel@sel4.systemsmailto:Devel@sel4.systems 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.