- Devel - lists.sel4.systems

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

Threads tutorial fails to initialize
by Weiqi Hu 31 May '20

31 May '20

Hi, I've tried to start the threads tutorial but it fails to initialize or create a build directory. Any hints for moving forward? weiqi@weiqi-ThinkPad-X250:~/sel4-tutorials-manifest-temp/threads$ sudo ../init --verbose --tut threads --solution Traceback (most recent call last): File "../init", line 96, in <module> sys.exit(main()) File "../init", line 85, in main args.task, initialised, tute_dir, build_dir, sys.stdout) File "/home/weiqi/sel4-tutorials-manifest-temp/projects/sel4-tutorials/common.py", line 100, in init_directories os.chdir(build_directory) FileNotFoundError: [Errno 2] No such file or directory: '/home/weiqi/sel4-tutorials-manifest-temp/threads_build'

2 2

Building picoserver example
by Russel emkil.minor 26 May '20

26 May '20

Dear seL4 developers, I am trying to built picoserver example https://github.com/seL4/camkes/tree/master/apps/picoserver <https://github.com/seL4/camkes/tree/master/apps/picoserver> using the following commands: $ ../init-build.sh -DPLATFORM=x86_64 -DCAMKES_APP=picoserver $ ninja But I am getting the following error: fatal error: pico_stack.h: No such file or directory Looks like I need to install libpicotcp. I found it here https://github.com/seL4/util_libs/tree/master/libpicotcp <https://github.com/seL4/util_libs/tree/master/libpicotcp> but no idea how to build and link to the example. Can you give me a hint how to proceed? Best regards, Ruslan Rezin.

2 1

seL4 Whitepaper Released
by Heiser, Gernot (Data61, Kensington NSW) 25 May '20

25 May '20

Dear seL4 community, I’m pleased to announce the seL4 Foundation whitepaper: The seL4 Microkernel – An Introduction This white paper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems. You can download it at https://sel4.systems/About/ Feedback welcome. Gernot PS: Some of you may have seen a pre-release version that was up on the Foundation web site since the Foundation launch. This is the complete version.

1 0

Trouble accessing linux guest through tun/tap
by Travis Wheatley 22 May '20

22 May '20

Greetings, I am working with the camkes-arm-vm qemu-arm-virt configuration. I started with the vm_minimal configuration and have added a tun/tap interface by creating the tap on my host thusly: # ip tuntap add tap0 mode tap # ip addr add 10.0.120.100/24 dev tap0 # ip link set dev tap0 up I have added support for what I beleive to be the appropriate interrupts by modifying my devices.camkes file thusly: vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; vm0.dtb_irqs = [35, 36, 37, 38]; Additionally, I have modified the settings.camkes thusly: if(${PLATFORM} STREQUAL "qemu-arm-virt") # force cpu set(QEMU_MEMORY "2048") set(KernelArmCPU cortex-a53 CACHE STRING "" FORCE) set(VmInitRdFile ON CACHE BOOL "" FORCE) set(VmPCISupport ON CACHE BOOL "" FORCE) set(VmVirtioNetArping OFF CACHE BOOL "" FORCE) set(VmVirtioNetVirtqueue ON CACHE BOOL "" FORCE) # set(qemu_sim_extra_args "-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01") set(qemu_sim_extra_args "-net nic,model=e1000 -netdev tap,id=mynet0,script=no,ifname=tap0 -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01") set(KernelArmExportPCNTUser ON CACHE BOOL "" FORCE) set(KernelArmExportPTMRUser ON CACHE BOOL "" FORCE) endif() This results in a tunl0 interface showing up on my linux guest. However, that interface does not have a mac address associated with it. I can use ifconfig to assign an IP address on the same subnet as the corresponding tap interface on the host. However, I can’t ping between the two. I thought this might be because I have VmVitruoNetArping set to OFF. However, I get compile time errors when I turn it on. Because the tunl0 inteface does not have the mac address specied in the qemu_sim_extra_args I am unsure of how to set up an arp table entry. Exctly what do I need to do to enable network communications between my linux guest and the host?

2 1

Help with creating a new project
by Yates, Tim 22 May '20

22 May '20

Hi, I am attempting to create a new CAmkES project. So far I have used the https://github.com/seL4/camkes-manifest.git repository and the https://github.com/SEL4PROJ/camkes-arm-vm-manifest repository and placed my .camkes file and components into the respective app folders for each. I then attempt to initialise my project as instructed here https://docs.sel4.systems/projects/camkes/ but it fails. It gives me the following error: hardware_gen.py: error: argument --dtb: can't open '/workspaces/microimpexor/seL4_build/build/kernel/kernel.dtb': [Errno 2] No such file or directory: '/workspaces/microimpexor/seL4_build/build/kernel/kernel.dtb' I am initialising my project with the following command: ../init-build.sh -DPLATFORM=qemu-arm-virt -DAARCH32=1 -DCAMKES_APP=appname -DSIMULATION=1 Some assistance on this matter would be greatly appreciated. Regards Tim Yates ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 1

some confuse about "bootstrap_use_current_simple" of bootstrap.c in libsel4allocman
by yadong.li 20 May '20

20 May '20

allocman_t *bootstrap_use_current_simple(simple_t *simple, size_t pool_size, void *pool) { allocman_t *allocman; int error; /* Initialize inside the current 1 level cspace as defined by simple */ allocman = bootstrap_use_current_1level(simple_get_cnode(simple), simple_get_cnode_size_bits(simple), simple_last_valid_cap(simple) + 1, BIT(simple_get_cnode_size_bits(simple)), pool_size, pool); if (!allocman) { LOG_ERROR("Failed to initialize an allocman"); return allocman; } ....... return allocman; } The params of "bootstrap_use_current_1level" below: cnode_size = simple_get_cnode_size_bits(simple), like 23, it is 8M endslot = BIT(simple_get_cnode_size_bits(simple)), also 8M I think we don't have so many endslot, because per slot is not only one byte Thank you very much

1 0

additional: some question about VisualCAmkES ？
by yadong.li 27 Apr '20

27 Apr '20

Hi， I found the VisualCAmkES tool can not parse grammar like import and marco in cmakes file, If I write very simple camkes file, only include one assembly and component. I want to know How can I use this VisualCAmkES tool to generate visual file in complex project like vm_minimal ? 发件人: yadong.li 发送时间: 2020年4月25日 21:06 收件人: 'devel(a)sel4.systems' 主题: some question about VisualCAmkES ？ Hi， I want to use VisualCAmkES for view，I follow the step of https://docs.sel4.systems/projects/camkes/visual-camkes/ I meet the below Problem， how can I resolve it ？ Thank you very much Syntax Error (u'/home/yadong.li/seL4_vm_11/ sel4_horizon/camkes-arm-vm/projects/vm/ apps/vm_cross_connector/vm_cross_connector.camkes:36:5: \x1b[31m\ x1b[1mVM_INIT_DEF\x1b[0m()', u' ', u"Syntax error in input at 'VM_INIT_DEF' (type ID) line 36 col 5", u"Syntax error in input at 'VM_GENERAL_COMPOSITION_DEF' (type ID) line 45 col 9", u"Syntax error in input at '(' (type _ANON_4) line 60 col 37")

1 0