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.... 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....

[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.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.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel