DOKK Library

Minutes of the 7th Meeting of the seL4 Board

Authors seL4 Project

License CC-BY-SA-4.0

Plaintext
                                                                                           The seL4® Foundation


       FOUNDATION
                                                                                https://sel4.systems/Foundation




 Minutes of the 7th Meeting of the seL4 Board
                           2022-02-24 to 2022-03-04 UTC
                                               By Email




Members present
   •   Gernot Heiser (GH) – Chair
   •   David Hardin (DH)
   •   Feng Zhou (FZ)
   •   Gerwin Klein (GK)
   •   Ian Xu (IX)
   •   June Andronick (JA)
   •   Olivier Engelkes (OE)
   •   Qiyan Wang (QW)
Observers present
   • Birgit Brecknell
   • Sascha Kegreiß


Members absent
   • Matthew Grosvenor (MC)
The meeting commenced at 23:40 on 2022-02-24 UTC.
   1. Confirmation of minutes of previous meeting
       RESOLVED: Draft minutes of 6th meeting, of 2021-10-06 UTC, are confirmed
   2. Matters arising from minutes of previous meetings
         • 210413: see item 5: Develop endorsement scheme for services and products
   3. Update from the Chair
       GH updated the Board on:
         • Handover of HENSOLDT Cyber’s Board seat from Sascha Kegreiß
           to OE
         • Appointment of Birgit Brecknell as Project Coordinator
         • Status of trademark applications
Copyright © 2022 seL4 Project a Series of LF Projects, LLC.
Distributed under the Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) License.
seL4 is a trademark of LF Projects, LLC.


                                                   1
    •   Membership development
    •   Community engagement
    •   TC-CoE Summit (with additional information from JA)
    •   Plans for next seL4 Summit
    •   Other ecosystem news
4. Update from the TSC Chair and matters arising
  GK updated the Board on:
    • Progress on large verification projects:
        – RISC-V confidentiality proofs completed
        – First of two refinement steps (“Refine”) for MCS completed
        – Delivery of projects contracted to Proofcraft
        – Commencement of verification work for AArch64
    • Community-accessible test infrastructure
    • community contributions
    • RFCs
    • new TSC member Yanyan Shen (NIO)
5. Endorsement scheme for services and products
  JA, on behalf of the CC, updated the Board on the recent deliberations regarding the
  Endorsement scheme. Following a cost-benefit assessment, the CC decided that:
    • For the foreseeable future there will only be an endorsement for services (not training
      or products)
    • Services endorsement will be limited to members and provided for free
    • Endorsement will be restricted to services from a standard list
    • Members may still list training and products, but they will not be endorsed.
6. Election process
  Under the Charter, the Board needs to approve the process for the upcoming Annual
  General Meeting and election of a general member representative for the Board.
  RESOLVED: The process for the election of the General Member representative will
  be the same as last year, ie a 2-week nomination process, conducted by email, with
  nominations to be sent to the seL4 Foundation, followed by a 1-week voting process,
  conducted by email, with votes to be sent to a returning officer to be designated.
  RESOLVED: The Annual General Meeting will be held via Zoom in two sessions to
  accommodate various time zones, namely:
    • 2022-04-06 07:00–08:30 UTC
    • 2022-04-06 23:00 – 2022-04-07 00:30 UTC
7. Adjustment of membership tiers
  RESOLVED by 2/3 majority (8 members in favour, 0 against, 1 absent): Effective
  2022-04-02, the membership fee structure, as a function of company size (given by the
  number of employees) will change as follows (the fee amounts will not change):




                                           2
                                 Size old          Size new      Fee
                                  1-499             1-99         $3k
                               500-1999          100-499        $10k
                              2000-4999         500-4999        $20k
                                 5000+            5000+         $30k

  8. Directing approved verification budget
     In the budget approved in the 6th Meeting, the Board set aside an amount of $100,000
     for a “Next roadmap item” for the seL4 verification, with the intent to allocate it later,
     depending on where other sources of funding became available.
     RESOLVED: The $100k “next roadmap item” to is to be used to start the “CRefine”
     step for the MCS kernel.
  9. Formalising the process for board meetings conducted electronically
     The Charter says that “unless all Board Members agree otherwise, they must receive at
     least 5 business days’ written notice of a meeting” and that “meetings may be conducted
     electronically, via teleconference, or in person at the discretion of the seL4 Board”.
     RESOLVED: When meetings of the Board are conducted by email, the following process
     will be used:
        • The Chairperson will email the Notice of the Meeting, including the Agenda, to
          Board members at least 48h before the start of the electronic meeting, allowing
          members time to consider the agenda and ask questions of a general nature;
        • at the beginning of the electronic Meeting, the Chairperson will start a separate
          email thread for each agenda item, with discussion and voting taking place in that
          email thread;
        • the electronic meeting will conclude 168h after it commenced, or earlier if all agenda
          items have been resolved;
        • the Chairperson may, at their discretion, extend the meeting if one or more agenda
          items remain unresolved 168h after the meeting commenced.
 10. Future meetings
     The next Board Meeting will likely be within 1–2 months after the election of the General
     Members representative (and the AGM), to elect office bearers, and approve a new
     budget. It will likely be held by email.
     We plan to hold an in-person/hybrid meeting co-located with the upcoming seL4 Summit
     (planned for October).
 11. AOB
     DH raised the issue of having more verified targets, especially popular platforms, such as
     the Raspberry Pi, and this should be funded by the Foundation.
     GK responded that multiple platforms for the same architecture are presently not
     supported by the seL4 verification framework and will require some fundamental changes.
     Proofcraft will take a proposal to the next Board Meeting.
All business having been dealt with, the meeting closed on 2022-03-04 at 0:02 UTC.

                                               3
ACTION SUMMARY

From        Item     Owner        Status       Action
22-02-25    11           GK        TBD         Proposal for supporting more verified platforms


Meeting Attendance
Current financial year, starting 2022-01-01:

                   Name                              Eligible     Attended
                   Gernot Heiser                        1             1
                   June Andronick                       1             1
                   Matthew Grosvenor                    1             0
                   David Hardin                         1             1
                   Olivier Engelkes                     1             1
                   Gerwin Klein                         1             1
                   Qiyan Wang                           1             1
                   Ian Xu                               1             1
                   Feng Zhou                            1             1


Acronyms

            TS     The   Trustworthy Systems research group at UNSW Sydney
            LF     The   Linux® Foundation
           TSC     The   Technical Steering Committee of the seL4 Foundation
            CC     The   Compliance Committee of the seL4 Foundation
            OC     The   Outreach Committee of the seL4 Foundation
           MC      The   Marketing Committee of the seL4 Foundation




 Signed as a true record
 2022-04-12




                                                 4