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: