- l4-hackers - example.com Site

L4Linux with L4Re and Fiasco.OC-UX
by Paul Boddie 04 Apr '19

04 Apr '19

Hello, I have been looking at trying out L4Linux in UX mode as a first step towards its use on "native" Fiasco, and I seem to be experiencing a problem with launching the Linux kernel itself. I have followed the instructions from these pages: https://l4linux.org/download.shtml https://l4linux.org/build.shtml https://l4linux.org/use.shtml Specifically, I have an existing build of UX that has been used for some time to develop software. I have updated it to revision 83 and have checked out the l4linux_requirements, which appear to be some packages (rtc and shmc) I already have. I then performed a build once again: make O=mybuild The L4Linux repository has also been checked out and updated to revision 83. The code has been configured and built using the following invocations: make O=mybuild x86_32-ux_defconfig make O=mybuild menuconfig # to set the L4Re build directory make O=mybuild Here, the mybuild directory is distinct from the L4Re mybuild directory. For the initial RAM filesystem, I downloaded the ramdisk-x86.rd file, and I run the system as follows: make O=mybuild ux E=L4Linux-basic After the usual familiar start-up messages, I see this output specific to the configuration being launched: ---- Ned: loading file: 'rom/l4lx.cfg' libio: Warning: Query of 'vbus' failed! PH 0 offs=00001000 flags=r-x PH-type=0x1 virt=00100000 evirt=0053f000 phys=00100000 ephys=0053f000 f_sz=0043f000 memsz=0043f000 PH 1 offs=00440000 flags=rw- PH-type=0x1 virt=0053f000 evirt=00a58000 phys=0053f000 ephys=00a58000 f_sz=0006ce9f memsz=00519000 PH 2 offs=00371ee0 flags=--- PH-type=0x4 virt=00470ee0 evirt=00470f1c phys=00470ee0 ephys=00470f1c f_sz=0000003c memsz=0000003c Starting binary at 0x100000, argc=6 argv=0xafff4f84 *argv=0xb1007ff4 argv0=rom/vmlinuz External resolver is at 0xa8000bd0 L4Re: rom/vmlinuz: Unhandled exception: PC=0x46980b PFA=97d47fe0 LdrFlgs=0 ---- In order to try and identify the problem, I used the following command: addr2line -e ~/L4/L4Linux/l4linux/mybuild/vmlinux 0x46980b This seems to indicate that the point of failure is at line 2727 in arch/l4/kernel/main.c which is the start of this function: int __ref L4_CV main(int argc, char **argv) So, I wonder what the problem might be that leads to a crash as the main function is being invoked. Have I missed anything obvious? All of this is being done in a Debian unstable chroot on x86. Paul

2 2

Raspberry Pi 3B and L4Linux
by Dejan Cotra 27 Mar '19

27 Mar '19

Hi all, Im trying to run L4Linux on Raspberry Pi 3B. So far I was able to build Fiasco kernel and L4Re for Raspberry Pi 3B. I used aarch64-linux-gnu-gcc toolchain. Also I was able to create Uboot image for hello config, which I successfully run on both qemu and Raspberry Pi 3B. So now Im trying to build L4Linux. First question would be does L4Linux supparm64 architecture? If yes, any hints for configuration? If it does not support arm64 architecture does this also mean that I have to build Fiasco kernel and L4Re for 32bit arm architecture. Thanks in advance, Dejan

2 1

Invalidating mapped flexpages in pagers
by Paul Boddie 19 Mar '19

19 Mar '19

Hello, I have been trying to implement a pager in L4Re where the pager employs a memory region of limited size to satisfy map requests for a dataspace occupying a larger virtual memory region. Upon receiving a map request, the pager identifies the dimensions of the flexpage to be sent to the task experiencing the page fault, and it populates the flexpage's memory with the appropriate data. What this accomplishes so far is that when page faults occur in a task accessing the dataspace, mappings from virtual memory addresses are established in the task referring to the memory region populated by the pager. The task can read from page to page and keep getting new data. However, as each new map request comes in, I want to be able to invalidate the mappings previously made by the pager. Otherwise, I get many pages in the task's address space referring to the same memory, which is obviously not what I intend. Is it possible to send a flexpage from the pager in such a way that the mappings previously established by Fiasco.OC for the memory region are invalidated? Or have I missed some other mechanism for achieving what I am attempting? The L4Re documentation isn't helping me so much here, and I can't seem to find examples of this kind of thing in the source distribution. Thanks for any help anyone can give! Paul

2 5

Huawei R&D lab in Dresden
by Martin Decky 07 Mar '19

07 Mar '19

[Apology for this job ad. Please ignore if you are not interested in job offers.] Dear all, Huawei is starting a new R&D lab in Dresden. The lab shall focus on microkernel OS design and development, with a well-balanced mix between innovative research (including, but not limited to, topics such as HW/SW co-design, heterogeneous computing, data-centric computing, etc.) and prototype development (including, but not limited to, design and implementation of key operating system services for Huawei's microkernel OS, safety and security certification, formal verification, etc.). We offer prospective job candidates the possibility to impact billions of Huawei devices, collaborate on real-world scenarios for the microkernel multiserver OS design (in the automotive, IoT, telco, industrial and other domains) and even influence future HW design (HiSilicon, one of the major semiconductor companies, is a fully owned subsidiary of Huawei). We are also supporting mutually beneficial collaboration with academia (e.g. ETH Zurich, TU Dresden) and microkernel-related companies. If you are interested in discussing the details of the senior engineer, software architect and researcher roles we offer, please do not hesitate to contact me. We will be also more than happy to talk to you at the upcoming Fachgruppe Betriebssysteme Frühjahrstreffen 2019 in Erlangen next week [1] and at EuroSys 2019 in Dresden in about three weeks [2]. [1] https://www.betriebssysteme.org/aktivitaeten/treffen/2019-erlangen/ [2] https://www.eurosys2019.org/ Best regards Martin Decky Senior Research Engineer Huawei Technologies German Research Center

1 0

Setting up ssd and hard disk in l4linux
by Xinyue Wu 26 Feb '19

26 Feb '19

Dear Developers, I have been trying to mount ssd and hard disk in l4linux. There are some similiar questions in previous archives, and I have done the following things according to them: - configure 'devs' file and 'io' file, add sata to vbus - enable PCI support - enable vPCI driver - enable AHCI driver But when I ran l4linux in hardware, I still couldn't find sata in pci bus, nor could I found my devices under /dev. Does anyone have some suggestions? Or maybe there are something wrong in my device configuration, please let me know if so. Thanks a lot. x86-legacy.devs ================= local Res = Io.Res local Hw = Io.Hw Io.hw_add_devices(function() SATA = Hw.Device(function() Property.hid = "SATA"; Resource.iop1 = Res.io(0x1f0, 0x1f7); Resource.iop2 = Res.io(0x3f6, 0x3f7); Resource.irq = Res.irq(14); end); end) l4lx-x86.io ==================== local hw = Io.system_bus() Io.add_vbusses { l4linux = Io.Vi.System_bus { -- Add a new virtual PCI root bridge PCI0 = Io.Vi.PCI_bus { pci_sata = wrap(hw:match("SATA")); }; }; } l4lx.cfg ====================== local L4 = require("L4"); loader = L4.default_loader; vbus_l4linux = loader:new_channel(); vbus_input = loader:new_channel(); loader:start( { caps = { sigma0 = L4.cast(L4.Proto.Factory, L4.Env.sigma0):create(L4.Proto.Sigma0); icu = L4.Env.icu; l4linux = vbus_l4linux:svr(); }, log = {"IO", "y"}, l4re_dbg = L4.Dbg.Warn, }, "rom/io rom/x86-legacy.devs rom/l4lx-x86.io"); loader:start( { caps = { vbus = vbus_l4linux; }, log = L4.Env.log:m("rws"), }, "rom/vmlinuz mem=1024M console=ttyLv0 earlyprintk=1 l4x_rd=rom/ramdisk-256m.rd root=1:0 ramdisk_size=268435456");

2 1

some questions about l4bd.c in l4linux
by yadong.li 20 Feb '19

20 Feb '19

Hi Adam， I am studying how to support emmc storage in L4Re. I have read the file l4linux/drivers/block/l4bd.c. I have some questions 1、 In “l4linux/drivers/block/l4bd.c”, I can’t find the function implementation of “l4fdxc_request_write” and some with prefix l4fdxc in l4linx or l4， is there some demos? 2、 If it is implemented by ourselves, where is more reasonable to place “l4fdxc_request_write” , in l4 or l4linux ? 3、 If in l4, Which implementation is more reasonable , lib or server? Thank you very much

2 1

Communication between L4Linux tasks and L4re tasks
by Canberk Demirsoy 16 Feb '19

16 Feb '19

Dear Developers, I have a simple question regarding the communication of L4Linux and L4re. I have already read previous entries but could not solve my problem. I am able to establish a communication between the tasks in L4re, but what I need is communication between a task that is running on L4Linux and a task that is running on L4re. How can I do this in simplest way? Any suggestions? Best Regards *Canberk*

2 1

Poll for Separation Kernel (microkernel) CC Protection Profile
by Holger Blasum 20 Jan '19

20 Jan '19

Hello l4-hackers, microkernel-based systems can be used as separation kernels[*] for security. At the moment there is a poll on input for a Common Criteria for Information Technology Security (CC) separation kernel protection profile draft, organized by a certMILS.eu colleague from Rostock Univ, at https://evasys.uni-rostock.de/evasys/online.php?p=ccuf-sk-wg The idea is to have a base protection profile (PP) that all players can agree with and to specify additional functionality as add-ons to the PP (e.g., in the form of PP modules). The questionnaire is an opportunity to provide early feedback. Note that there are no mandatory questions, i.e. you can freely move around / you can leave any question unanswered - the only condition for your feedback be submitted to the collection system is that you go to the last page and use the submit button there. We invite feedback via that poll by end of this week. If, beyond the questionnaire, you want to join the Common Criteria User's Forum separation kernel working group, or anyone would like to have more time, just let me know by answering to this email. [*] https://en.wikipedia.org/wiki/Multiple_Independent_Levels_of_Security Best, -- Holger Blasum, SYSGO

1 1

QEMU advent calendar
by Matthias Lange 21 Dec '18

21 Dec '18

Hi, today we have another small treat for those interested in L4Re. You should check door 21 [1] of the QEMU advent calendar for a peek on what you can build with our newly released #L4Re projects. Happy holidays! Matthias. [1] https://www.qemu-advent-calendar.org/2018/#day-21 -- Matthias Lange, matthias.lange(a)kernkonzept.com, +49-351-41 888 614 Kernkonzept GmbH. Sitz: Dresden. Amtsgericht Dresden, HRB 31129. Geschäftsführer: Dr.-Ing. Michael Hohmuth

1 0

New L4Re projects released
by Matthias Lange 20 Dec '18

20 Dec '18

Dear L4 folks, as the year is slowly coming to an end we want to take the opportunity to announce the release of new L4Re projects to our github [1]. This release includes the development version of our small virtual machine monitor uvmm [2]. It is capable of running Linux on all three of L4Re's supported architectures. Another noteworthy project is io [3] which is our IO device multiplexing and virtualizing component. To get you started we added a new tutorial [4] on how to setup and run a Linux VM on L4Re. We hope you enjoy the new release and we love to hear what you think. Happy holidays! Matthias. [1] https://github.com/kernkonzept [2] https://github.com/kernkonzept/uvmm [3] https://github.com/kernkonzept/io [4] https://github.com/kernkonzept/manifest/wiki/LinuxVM -- Matthias Lange, matthias.lange(a)kernkonzept.com, +49-351-41 888 614 Kernkonzept GmbH. Sitz: Dresden. Amtsgericht Dresden, HRB 31129. Geschäftsführer: Dr.-Ing. Michael Hohmuth

1 0