June 2020 - Devel - lists.sel4.systems

RISC-V (RV64) is the third ISA with verified seL4
by Heiser, Gernot (Data61, Kensington NSW) 09 Jun '20

09 Jun '20

Dear seL4 community, I’m extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. My blog discusses provides a bit more context for this announcement: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/ What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. Gernot for the Trustworthy Systems team and the seL4 Foundation

1 0

seL4 + TrustZone: Spanning both worlds
by Nick Spinale 08 Jun '20

08 Jun '20

On TrustZone-enabled Arm systems, seL4 could span both the secure and normal worlds. To do so would require extending untyped and frame capabilities with a bit associating them with either the secure or non-secure physical address space. In this email, I’ll touch on what a software stack based on this idea might look like, why that’s interesting, and exactly what extensions to the kernel it would require. I’m interested in your thoughts and feedback on this informal proposal. If there’s interest, I’ll draft a patch to illustrate it more precisely. # TrustZone background The security of a TrustZone-enabled system is achieved by partitioning all of the SoC’s hardware and software resources so that they exist in one of two worlds - the secure world for the security subsystem, and the normal world for everything else. From the point of view of an ARMv8-A processor, the system has two physical address spaces: one for secure transactions and another for non-secure transactions. Page table entries contain a field called the NS (non-secure) bit, which determines whether a page is mapped from the secure or non-secure physical address space. Furthermore, the processor state contains a global NS bit, which can only be modified by software executing at the highest exception level, EL3. When the NS processor state bit is set, the processor is said to be executing in the non-secure state, and can’t issue secure bus transactions, regardless of the values of the NS bits in its translation tables. A typical TrustZone software stack hosts a TEE (Trusted Execution Environment) on secure-world resources, and a REE (Rich Execution Environment) on normal-world resources. A so-called “secure monitor” runs in EL3, and uses the NS processor state bit to implement a coarse context switch called a “world switch”. The simplicity of this coarse context switch minimizes the attack surface of the secure monitor. # seL4 + TrustZone A formally verified microkernel such as seL4 can be trusted to protect secure hardware resources, and the TEE they host, using translation tables alone. That is, seL4 allows for a design where the processor always runs in state NS=0 (“secure state”), and normal-world software is restricted to non-secure world hardware resources using just the NS bits in the translation tables controlled by seL4. Such a software stack, with seL4 spanning both the secure and non-secure worlds, is attractive on multiple fronts. seL4 provides a higher level of assurance than typical EL3 monitor firmware, which we can now eliminate from the TCB. seL4 also provides a richer API than typical EL3 firmware, allowing for security critical secure-world components to be developed and verified at a higher level of abstraction. Furthermore, while the two-world model is organized around just one strong security boundary, seL4 allows for an unbounded number of equally strong security boundaries, as isolation is based on translation tables rather than the less flexible NS processor state bit. This design allows a seL4-based system to utilize non-secure hardware resources, while protecting the kernel and sensitive components inside secure hardware resources. This permits a threat model similar to that of a typical TrustZone-based TEE (such as OP-TEE or Trusty), which includes some hardware attacks, but without limiting seL4 userland components to the secure world alone. Such a software stack has been especially interesting since the release of ARMv8.4-A, which enables EL2 in the secure state (S-EL2). seL4 running in S-EL2 can host a rich operating system such as Linux to drive non-secure hardware resources. Compare this to a seL4-based software stack running a Linux VM without the help of TrustZone. In particular, consider a case where the Linux VM drives most of the hardware platform’s devices via direct passthru access. Reasoning about the interactions between hardware components on a SoC is difficult. Even after correctly programming the SMMU, a great deal of SoC-specific detail must be covered in order to convince yourself that a driver or VM can’t violate its isolation indirectly through a device within its reach. This sort of reasoning is an active area of research (see, for example, the Barrelfish OS project). However, for use cases where the trust model aligns with the SoC’s boundary between secure and non-secure hardware resources, TrustZone provides a straightforward means of ensuring the protection of critical software components from those with access to non-secure devices. # Extending seL4 Currently, untyped objects are either general purpose memory or device memory. To support the design I’ve proposed, untyped objects would need to be extended with another dimension: secure memory or non-secure memory. Non-secure general purpose memory would be subject to the same restrictions as device memory, with the exception that frames derived from non-secure general purpose untyped may be used as IPC buffers. Unlike the general-purpose/device dimension, the secure/non-secure dimension affects the mapping of a frame. The kernel would set the NS bit in page table entries according to whether that frame is secure. This extension would require modifying just a few lines of code in the kernel itself and would, of course, be optional and configurable. - - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - - The ideas presented in this email constitute research activity at Arm rather than an official position or recommendation. IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

3 3

Difficulty booting guest kernel on zcu102
by Travis Wheatley 04 Jun '20

04 Jun '20

I’ve been working with a VM and docker container created by the good folks at DornerWorks. I had a compile time error with the camkes-arm-vm-manafest tree called out in their "Getting Started” lab. However, I was able to successfully compile an image using the instructions and files in their single_vm_lab. I am loading that image onto an SD card with their pre-built boot.bin. At the U-boot prompt I load that image to 0x10000000 and subsequently type “go 0x10000000”. The image seems to start the initial boot just fine but I get an exception when it tries to jump to the kernel. image entry point. Looking at the value of esr_eli1 it appears that something is trying to write to a protected register. Wondering if there is some sort of switch setting on the board or special flags that need to be sent to u-boot to keep this from happening. Here is the console output: ZynqMP> fatload mmc 0 0x10000000 dorner 22183936 bytes read in 1472 ms (14.4 MiB/s) ZynqMP> go 0x10000000 ## Starting application at 0x10000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[10000000..1152e06f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 100f4058. Loaded DTB from 100f4058. paddr=[237000..23bfff] ELF-loading image 'kernel' paddr=[0..236fff] vaddr=[ff8000000000..ff8000236fff] virt_entry=ff8000000000 ELF-loading image 'capdl-loader' paddr=[23c000..1854fff] vaddr=[400000..1a18fff] virt_entry=4088d0 ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point... ELF-LOADER: Synchronous exception received: esr_el1: 86000004 elr_el1: ff8000000000 spsr_el1: 600003c5 far_el1: ff8000000000 abort() called.

1 0

Builds
by Matt Youill 04 Jun '20

04 Jun '20

Hi, Am in the process of learning seL4 and have managed to get, build and run the tutorials, which is great. Now looking at creating an application and I have a question about seL4 builds. The documentation here... https://docs.sel4.systems/projects/buildsystem/incorporating.html refers to a build setup that AFAICT is different to the reference application, which I think is here... https://github.com/seL4proj/sel4webserver Which is the best approach to follow? Best, Matt

2 1

Re: [seL4] Threads tutorial fails to initialize
by Weiqi Hu 04 Jun '20

04 Jun '20

Thank you for the suggestion but it seems like I need to access the init file one directory above. In the case of seL4test and build-x86 it needs to be init-build.sh On Sun, May 31, 2020 at 9:14 AM laokz <laokz(a)foxmail.com> wrote: > Hi Weiqi, > > Did you try init-build.sh( > https://docs.sel4.systems/GettingStarted#setting-up-your-machine)? I > recall this like issue before. > > Regards, > laokz > > I tried adding the --plat argument but it's the same error. Also, no build > directory was created on the attempts. > > I didn't have the same problem with the capabilities, untyped, and mapping > tutorials but it appears something is different for the threads tutorial. > > On Sat, May 30, 2020 at 5:11 PM Chubb, Peter (Data61, Kensington NSW) < > Peter.Chubb(a)data61.csiro.au> wrote: > > > >>>>> "Weiqi" == Weiqi Hu <weiqi.hu(a)gmail.com> writes: > > > > Weiqi> Hi, I've tried to start the threads tutorial but it fails to > > Weiqi> initialize or create a build directory. Any hints for moving > > Weiqi> forward? > > > > Looks like you omitted the --plat argument. > > > > Try > > ../init --plat pc99 --tut threads --solution > > > > You may need to delete the build directory before this will work. > > > > -- > > Peter Chubb Tel: +61 2 9490 5852 > > http://ts.data61.csiro.au/ > > Trustworthy Systems Group CSIRO's > Data61 > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > >

2 2

constituting seL4 TSC meeting
by Klein, Gerwin (Data61, Kensington NSW) 03 Jun '20

03 Jun '20

The technical steering committee (TSC) of the seL4 Foundation had its constituting meeting on 20 May, and the meeting minutes [1] are now published on the TSC page of the foundation [2]. The TSC is the body that sets the technical direction of seL4 and its proofs, including processes, contributions, documentation, etc. This first TSC meeting was mostly about processes and setting things up — future TSC meetings are planned to be public, and will be announced on this mailing list. One of the first things the TSC would like to do is make seL4 and its related repositories easier to contribute to. You may have seen a few things that already have happened: - more content on the docs site at foundation launch - DCO instead of CLA - first direct github CI tests that run on pull requests for the seL4 and l4v repos Some of the things we are planning to do: - make seL4 code and proof regression tests available directly on github as much as possible, to make it easier to see what breaks verification and what not - open up issues and pull request management more to the community so that pull requests can become less of a bottleneck - publish the source of the sel4.systems site, so people can make contributions - more documentation for the proofs If you have ideas what else the TSC could do to encourage contributions, please let us know! Either here on the mailing list, or if you prefer, by email to me directly. Cheers, Gerwin (for the TSC) [1]: https://sel4.systems/Foundation/TSC/notes/tsc-meeting-2020-05-20.pdf [2]: https://sel4.systems/Foundation/TSC/

1 0

UNSW seL4 teaching videos available
by Heiser, Gernot (Data61, Kensington NSW) 02 Jun '20

02 Jun '20

Dear seL4 community, I’m pleased to announce yet another contribution of UNSW Sydney to the seL4 community: This year I’m making the seL4-related videos from my UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel: https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site: https://www.cse.unsw.edu.au/~cs9242/current/ Enjoy, Gernot

2 1

mcs kernel compatible with camkes project
by Parvaneh Ahgajani 02 Jun '20

02 Jun '20

Hello all, I wanted to use camkes to create real-time application. In periodic application, it mentioned that "_period" and "_budget" only have affect on the MCS kernel. I tried to build application with kernel version 11.0.0-dev but it doesn't work. I wanted to know how I can have access to MCS kernel that is compatible with camkes project. Thank you, Parvaneh Aghajani.

2 1