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