- Summit-pc - lists.sel4.systems

seL4 summit 2023: reviews
by Birgit Brecknell 12 May '23

12 May '23

Dear PC, It’s reviewing time! You should all have received a link to your review file. As previously said the review process should be really light weight. The aim is to put together an interesting program that we want to listen to, or we think others in the community would like to listen to. You’ve all been assigned 8-10 of the submissions —except Darren and Ihor, who will read them all. Feel free to read more (they are really short) and rate them if you want. The allocation is semi-random, and conflict-of-interest (in the reviews and in the live discussion) will be handled quite openly: declare if you have a conflict, but your opinion/knowledge is still welcome. So your job is: 1- read the abstracts you’ve been assigned (or more if you want). 2- rate them in column H (with A+, A, A-, U = Undecided, R = Reject, S = suggest a repurpose (panel, BoF..)). 3- add comments in column I; this is optional but is really useful for (a) you to remember the reasons of your rating in the discussion meeting :) and (b) if you can’t attend the discussion for any reason, we’ll know more about the reasons of your rating. 4- while you review, please start thinking about invited speakers, i.e. if some of these talks could be turned into invited talks, or if the topic makes you think about a good invited talk idea from someone else. We will discuss invited talks soon and it’s a good moment to start thinking about it. 5- if reading the reviews makes you think about some seL4 work that has not been submitted but would be a good addition, please let me know. If we agree, I can follow-up to see if they would be happy to participate. And please do all this before 12 May so we have time to collate all the answers before the "PC meeting” on 18-19 May (which you should all have received an invitation for). If you have any questions, please don’t hesitate to ask. Many thanks for your work on this, it is appreciated :) cheers Birg & June --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW birgit.brecknell(a)unsw.edu.au 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

2 2

seL4 summit 2023: reviews meeting (zoom link)
by Birgit Brecknell 21 Apr '23

21 Apr '23

https://unsw.zoom.us/j/84805656644

1 0

seL4 summit PC: time slot for reviews meeting
by Birgit Brecknell 21 Apr '23

21 Apr '23

Dear PC It's almost reviewing time! As previously said, the review process will be light weight. The aim is to put together an interesting program that we want to listen to, or that we think others in the community would like to listen to. In short, your job will be to Review 5-10 short abstracts over 2-3 weeks (<3h of work) The review period will be 26 April - 17 May More details to follow re the actual reviewing process. Join a meeting to discuss reviews, finalise acceptance, discuss keynotes (2h) Finding a meeting time that works across the timezones is difficult. We have two dates and ranges available for the 2-hour meeting: Wed 17 May, 7am-11am Syd time Fri 19 May, 7am-11am Syd time Can you please go to http://whenisgood.net/x9j33f5 to let us know which dates/2-hr blocks suit you? If none suit, please say "none" in the comments box. We'll ask people who can't make it to send their reviews and suggestions via email. Many thanks for your work on this, it is very much appreciated. cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

2 3

Fwd: [seL4 Announce] seL4 summit: deadline extension to 24th of April
by June Andronick (seL4 Foundation) 31 Mar '23

31 Mar '23

Dear PC members, As you will have seen, we have extended the deadline to submit a talk by 2 weeks, for the reasons explained below. An updated rough timeline for reviewing period is on: https://docs.google.com/spreadsheets/d/1Tz-ITT6O9GIAl5yNm1QDMYg_hKJ0TZD5pL4… **Please encourage submissions in your network, contacts, customers, partners…** :) If you have any specific people/work you’d like to hear about, please nudge/ping explicitly, or let me know and I’ll do it :) Many thanks June > Begin forwarded message: > > From: Announcements about seL4 -- low volume list <announce(a)sel4.systems> > Subject: [seL4 Announce] seL4 summit: deadline extension to 24th of April > Date: 31 March 2023 at 4:36:21 pm AEDT > To: Announcements about seL4 -- low volume list <announce(a)sel4.systems>, devel(a)sel4.systems > Reply-To: announce(a)sel4.systems > > The deadline to submit a presentation to the seL4 summit 2023 is extended by 2 weeks. You now have until the 24th of April 2023 to propose a talk, by uploading an abstract of one page or less to: > https://sel4.systems/Foundation/Summit/2023/submit > > The reason for the extension is that we want to let you know the definite dates for the summit before the deadline :) Current tentative (and very likely) dates are 19-20-21 September 2023, to be confirmed very soon. > > Looking forward to receiving your proposals. We want to hear about your cool seL4 work! > > And spread the word! If you want to hear about specific seL4 work, ping people around you or let us know at summit(a)sel4.systems <mailto:summit@sel4.systems> > > June > _______________________________________________ > Announce mailing list -- announce(a)sel4.systems > To unsubscribe send an email to announce-leave(a)sel4.systems

1 0

(seL4 summit 23): share the CfP!
by June Andronick (seL4 Foundation) 20 Feb '23

20 Feb '23

Dear PC for the seL4 summit 2023, The Call for Presentations is out! [0] [1] We now count on all of you to circulate it in your own circles and encourage people to submit :) Remember, the aim is to assemble the program that we would really be keen to hear about (or that we think the community should know and hear about). So don’t hesitate to nudge specific people you’re keen to hear from and encourage them to submit. You can also let us know if you’d prefer that we contact them. Also note that we have slightly updated the technical planning, shifting it to take the delay into account: https://docs.google.com/spreadsheets/d/1Tz-ITT6O9GIAl5yNm1QDMYg_hKJ0TZD5pL4… Let us know if you have any questions, and thanks! June, Birg, Darren, Ihor [0] https://sel4.systems/Foundation/Summit/2023/cfp [1] https://www.linkedin.com/feed/update/urn:li:ugcPost:7033324568924618753/

1 0

Meet your fellow PC members + 2 small tasks
by June Andronick (seL4 Foundation) 13 Feb '23

13 Feb '23

Dear PC of the seL4 Summit 2023! We are thrilled that you accepted the invitation! Please find below [0] our awesome team, from various parts of the seL4 ecosystem. To get started, we have 2 small tasks for you: 1- Website: we aim to announce the PC next week, so please check, by Friday 10 Feb, that you are fine with your name/affiliation/link as below [0]. If we don't hear back from you, we'll assume it's all good and we'll go ahead with the announcement. For the people that were on the PC last year, we'll use the same picture as last year. If you prefer a different one, please send it to Birg and I by Friday as well. 2- Themes/topics for the Call for Presentations: we suggest we keep the same topics as last year [1], as they are still good and relevant. But your thoughts/suggestions are welcome. Please send them by Tuesday 14 Feb. If we don't hear back from you, we'll assume you're fine with reusing the same topics and we'll aim to publish the CfP around Wednesday 15th Feb. Your next task (hopefully next week) will be to help advertise for the CfP, encourage submissions, nudge specific people you'd like to hear about etc. Remember: we aim to maximise the take away value. So you should think of it as: what would an ideal seL4 summit look like for you? What is the cool seL4 work that you heard about and would love to hear more about? The Call For Presentation is lightweight and informal. The aim is to attract the work we want to hear about or want the community to hear about. I’m just adding a 3rd tiny task: 0- if you don’t need to reply to 1 and 2 above because you happen to be fine with the default, can you please still send Birg and I an “ACK” email so we know we got the mailing list right? :) If you have any questions, let us know. Thanks again, Birg, June, Darren & Ihor [0] PC of the seL4 Summit 2023: - Darren Cofer (Raytheon), co-chair, http://loonwerks.com/people/darren-cofer.html - Ihor Kuz (Kry10), co-chair, http://www.ikuz.org/ - Perry Alexander (U of Kansas), https://perry.alexander.name - June Andronick (Proofcraft), https://proofcraft.systems/#june - Todd Carpenter (Adventium Labs), https://www.adventiumlabs.com/team-member/todd-carpenter - Martin D2 (NCSC), https://www.ncsc.gov.uk - Alison Felizzi (Kry10) - Axel Heider (Hensoldt Cyber), https://www.linkedin.com/in/axelheider/ - Gernot Heiser (UNSW), https://trustworthy.systems/people/?cn=Gernot+Heiser - Lucy Parker (UNSW), https://trustworthy.systems/people/?cn=Lucy+Parker - Nick Spinale (Colias Group), https://nickspinale.com - Robbie VanVossen (Dornerworks), https://www.linkedin.com/in/robbie-vanvossen-gr/ [1] Themes for the seL4 summit’22 CfP: - seL4 on-going and planned R&D, mature or early stage: - seL4 research efforts - seL4 development efforts - work-in-progress seL4 development - student work on seL4 - new/missing/next-gen kernel mechanisms - seL4-related roadmaps: what you plan to work on and when - seL4 grand challenges - OS frameworks and services - seL4 userland with programming language support beyond C - High performance systems based on seL4: pushing the boundaries - seL4 experience reports - experience with deploying seL4 in the field, in commercial/deployed products - experience with teaching seL4 - experience with seL4 in certification schemes and application of industry standards - experience with “building a business case for using a verified kernel” - experience with porting software from other OSes - seL4 and hardware - ports to new hardware platforms or architectures - multicore systems - virtualisation - new/proposed hardware features or architectures, which could also enable or broaden the scope of formal reasoning (e.g. about time protection) - seL4 in embedded processors on FPGAs, and impact of assured separation - IOMMU solutions for various hardware architectures and impact for seL4 - seL4 and assurance: - application-level verification leveraging seL4 proofs - correctness, spatial separation, temporal separation, and real-time proofs - formalised interface between or composition of kernel-level proofs and user-level proofs - verification engineering at scale, scaling verification productivity - security/safety impact/assurance/certification for an seL4-based system

1 1

seL4 summit'23: 2 questions for you (by 26 Jan)
by June Andronick (seL4 Foundation) 08 Feb '23

08 Feb '23

Dear PC members of the seL4 summit 2022, Thanks again for serving in last summit’s PC. Now is time to work on the summit’23 :) starting with forming the PC. Firstly, I’m very glad to announce that Ihor has accepted to be the new “junior” co-chair for this year and Darren accepted to stay on board for another year as the “senior” co-chair. Many thanks to both of them. Now can you please all reply to me (CCing Birg): (a) telling me whether you would be happy to be on the PC for 2023 or not, and (b) suggesting 1 name for a new PC member we might want to consider (with a few words why if it’s not obvious). Some diversity in all dimensions would be great, as much as feasible. Current PC can be found on https://sel4.systems/Foundation/Summit/home.pml From there we will aim for a mix of "old and new blood” :) Please reply by the 26th Jan or earlier. If you need more time let me know. See below for a rough timeline for the PC work [0] and reminder of expected duties and load [1]. It should be as lightweight (and hopefully fun) as last year :) Oh and the vote for the location resulted in Minneapolis, and the dates we’re looking at would hopefully be either the week of Sep 18 or the week of Oct 9 (3 days to be determined in these weeks). Any questions let me know. Many thanks! June [0] https://docs.google.com/spreadsheets/d/1Tz-ITT6O9GIAl5yNm1QDMYg_hKJ0TZD5pL4… [1] The Program Committee is in charge of the technical side of the event (content, invited speakers, program…). The PC process aspires to be quite informal, lightweight and efficient, with the aim of producing the most interesting and engaging event. There will be an open call for presentations; submissions will be short abstracts. The commitment required from the PC should be very light (equivalent to less than 2 full days, spread over a long period) and the PC will receive all the necessary admin support (to track, chase-up, send emails etc) from Birgit (CC-ed) and myself. There is also an informal Steering Committee made of Gernot, Gerwin and myself for any oversight. Duties and rough commitment estimate can be summarised as follows (with a rough timeline in [0]): - Reply to this email and suggest a name for a new PC member (<1h) - Provide feedback/suggestions for themes for CFP (<1h) - Advertise, use own network to attract submissions, nudge specific people to submit (<1h) - Review 5-10 short abstracts over 2-3 weeks (<3h of work) - Meeting to discuss reviews, finalise acceptance, discuss keynotes (2h) - Provide feedback on program (<1h) - Volunteer for session chair - Attend if possible, help with chairing, make it a successful event

1 2

Re: seL4 summit 2022 - Draft program: pls check by COB 27 Jun
by Cofer, Darren D Collins 25 Jun '22

25 Jun '22

Looks good to me. Darren ________________________________ From: Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> Sent: Friday, June 24, 2022 2:07:47 AM To: summit-pc(a)sel4.systems <summit-pc(a)sel4.systems> Subject: [External] seL4 summit 2022 - Draft program: pls check by COB 27 Jun Dear Presenters and PC Please find attached the draft program for the seL4 Summit 2022. NB: We haven't finalised all the talk titles, presenters and affiliations. Action item: Please check the program and let us know if there are any problems with it. Please do this by COB Mon 27 Jun, so that we can advertise the program next week. Many thanks, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

seL4 summit: finalised draft program --please check!
by June Andronick (seL4 Foundation) 13 Jun '22

13 Jun '22

Hi all, please find attached a finalised draft program. I’ve managed to fit everything in, but it’s tight! We’ve got a packed program, and a nice one :) Can you please check it and send me any concern within a few days? We’d like to send notifications Wed next week. Don’t worry about the titles, we’ll ask for finalised one when sending the notifications. Thanks! June AMA = Ask Me Anything BoF = Birds of a Feather

2 1

Fwd: Submission to seL4 Summit - Timing Channels
by June Andronick (seL4 Foundation) 01 Jun '22

01 Jun '22

FYI: ETH can give a talk on hardware support to prevent timing channels. > Begin forwarded message: > > From: "June Andronick (Gmail)" <june.andronick(a)gmail.com> > Subject: Re: Submission to seL4 Summit - Timing Channels > Date: 1 June 2022 at 9:24:50 am AEST > To: Nils Wistoff <nwistoff(a)iis.ee.ethz.ch> > Cc: summit(a)sel4.systems, Gernot Heiser <gernot(a)unsw.edu.au>, Luca Benini <lbenini(a)iis.ee.ethz.ch> > > Hi Nils, > > Thanks for your submission! We’ll come back to you once we’ve worked out the program. > > Cheers > June > >> On 30 May 2022, at 9:01 pm, Nils Wistoff <nwistoff(a)iis.ee.ethz.ch> wrote: >> >> Dear program committee, >> >> Hereby I would like to apply for a presentation at the seL4 summit 2022. >> >> Title: >> Hardware Support for Preventing Microarchitectural Timing Channels >> >> Abstract: >> Microarchitectural timing channels enable information transfer between security domains that are supposed to be isolated, bypassing the operating system's security boundaries. They result from shared microarchitectural state that depends on execution in one security domain and impacts timing in another. Since modern ISAs do not specify timing behaviour, they are insufficient to address these channels. >> >> In this talk, we present fence.t, a novel RISC-V instruction that clears the processor's microarchitectural state and thus any timing dependence on execution history. We show how this instruction was implemented in an open-source RISC-V core and integrated into an experimental version of seL4 with time protection. Furthermore, we will address the challenges of fence.t and its future roadmap. >> >> I am looking forward to your response! >> >> With best regards, >> Nils Wistoff >> >> -- >> Nils Wistoff >> PhD Student >> Integrated Systems Laboratory (IIS) - ETH Zurich >> ETZ J85 >> Gloriastrasse 35 >> CH-8092 Zurich >> +41 44 632 06 75 >> nwistoff(a)iis.ee.ethz.ch >> >

1 0