Data61 Seeking Research Scientist
=================================
We are looking for a full-time research scientist in formal verification to
join us, the Trustworthy Systems group, at Data61, CSIRO. Our highly
international team is located on the UNSW campus, close to the beautiful
beaches of sunny Sydney, Australia, one of the world's most liveable cities.
Our vision is a world in which computer users can choose all three: correct,
secure, and fast. We believe that most current approaches to building systems
are fundamentally flawed. We aim to demonstrate a better way. Our approach is
rooted in foundational, formal verification using theorem provers (e.g.,
Isabelle, HOL4), and high-performance system design. If you find this vision
appealing, and have ideas about how to pursue it, we want to hear from you.
Our team brings together a unique combination of expertise in systems,
security, formal verification, and programming languages. We are the creators
of seL4, the world's first operating system microkernel with a
machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance
and foundational binary-level correctness and security proofs. We are also
involved in CakeML, the most realistic verified compiler for a functional
programming language, and a promising approach to scaling full verification
up to applications code.
We are building on these successes in various directions, including
concurrency (formal reasoning and implementation), timing (real-time
guarantees and timing channels), and whole-system verification using
component systems (e.g., CAmKES) and code+proof co-generation.
We publish in top conferences, and are involved in multiple international
research collaborations. You will have the opportunity to teach at UNSW
should you wish to take it. We have a flexible, friendly, and intellectually
stimulating work environment.
We value diversity in all forms and welcome applications from people of all
ages, including people with disabilities, and those who identify as LGBTIQ.
See https://ts.data61.csiro.au/diversity/ for more information.
The salary range for this position (plus superannuation) is
- Research Scientist: 97k-105k
- Senior Research Scientist: 111k-130k
depending on experience and qualifications.
Apply online here:
https://jobs.csiro.au/job/Sydney%2C-NSW-Research-ScientistSenior-Research-S…
Your application should include a cover letter, CV, short research statement,
and contact information for two references.
This round of applications closes on 15 January 2019.
For any questions on this position, please contact June.Andronick(a)data61.csiro.au
Data61 Seeking Proof Engineers
==============================
We are are hiring again!
If only there were a place where I could prove theorems for money,
change the world, and have fun while doing it...
Sounds too good to exist?
In the Trustworthy Systems team at Data61 that's what we do for a
living. We are the creators of seL4, the world's first fully formally
verified operating system kernel with extreme performance and strong
security & correctness proofs. Our highly international team is located
on the UNSW campus, close to the beautiful beaches of sunny Sydney,
Australia, one of the world's most liveable cities.
We are looking for multiple motivated proof engineers who want to join
our team in Sydney, move things forward, and have global impact. You
would
- work on industrial-scale formal proofs in Isabelle/HOL
- develop formally verified infrastructure for building secure systems
on top of seL4
- contribute to improved proof automation and reasoning techniques
- apply formal proof to real-world systems and tools
To apply for this position, you should possess a significant subset of
the following skills.
- functional programming in a language like Haskell, ML, or OCaml
- first-order or higher-order formal logic
- basic experience in C
- ability and desire to quickly learn new techniques
- undergraduate degree in Computer Science, Mathematics, or similar
- ability and desire to work in a larger team
We are hiring at two levels, so if you are more qualified or
experienced than the above would suggest, you can come in as a senior
proof engineer.
If you additionally have experience
- in software verification with an interactive theorem prover such as
Isabelle/HOL, HOL4, or Coq, and/or
- with operating systems and microkernels
you should definitely apply!
If you have the right skills and background, we can provide training on
the job. Continual learning is a central component of everything we do.
You will work with a unique world-leading combination of OS and formal
methods experts, students at undergraduate and PhD level, engineers,
and researchers from 5 continents, speaking over 15 languages.
Trustworthy Systems is a fun, creative, and welcoming workplace with
flexible hours & work arrangements.
We value diversity in all forms and welcome applications from people of
all ages, including people with disabilities, and those who identify as
LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information.
Salary ranges, in AUD (plus superannuation):
- Junior Proof Engineer: 73k-93k
- Senior Proof Engineer: 97k-105k
depending on experience and qualifications.
Apply online at the following link for the Proof Engineer positions:
- https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/518443000/
- https://jobs.csiro.au/job/Sydney%2C-NSW-DATA-61/518441000/
Your application should include a cover letter, CV, undergraduate
transcript (if applicable), and contact information for two references.
This round of applications closes on 17 December 2018.
For any questions on these positions, please contact
Rafal.Kolanski(a)data61.csiro.au or June.Andronick(a)data61.csiro.au
The seL4 code and proof are open source. Check them out at https://seL4.systems
More information about Data61's Trustworthy Systems team at
https://ts.data61.csiro.au
There are additional proof engineering positions available on the
Cogent project. Cogent is a language we designed to ease the
verification of systems components around seL4. For expressions of
interest, see contact details on
https://ts.data61.csiro.au/projects/TS/cogent.pml
Looking to do a PhD?
Data61 and UNSW (https://www.unsw.edu.au/) offer scholarships!
See https://ts.data61.csiro.au/students/research.pml for details.
Hello,
the time spend by a vCPU TCB (tcbTimeSlice) seems to be not
accounted/updated by the seL4 kernel on a timer ticks, which leads to
starvation of other TCBs running on the same or lower priority level.
In one of our test setups, if once a vCPU runs and doesn't give up its
timeslice willful (e.g. guest goes in while loop and thereby not causing
a VM exit to be handled by the VMM), all other TCBs (normal threads and
vCPUs) on the same timeslice are not considered to be scheduled again,
since tcbTimeSlice of the vCPU stays full forever.
Following patch seems to fix the issue. Can you please have a look and
verify that it is correct ? Or should it be solved on another place in
the kernel differently.
Just out of curiosity, why is a separate thread state in the scheduler
for x86 (CONFIG_VFX) required that is not needed for scheduling of a
vCPU on ARM ? I didn't expect the scheduler thread states to be
different between hardware architectures in seL4.
Cheers,
--
Alexander Boettcher
Genode Labs
https://www.genode-labs.com - https://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
HI, I have a question about sel4bench IPC.
Thanks for the reply.
1. Making seL4_IPCBuffer and mapping into the thread is necessary?
I think that sending short messages don't need seL4_IPCBuffer, is it right?
2. This is seL4_Call annotation in benchmark_param.
/* Call fastpath between client and server in the different address space */
But I can't understand how to measure seL4_Call function performance.
[Client thread] [Server thread]
seL4_Call seL4_ReplyRecv(I'm not sure)
1) client send message.
2) server receive message.
3) server send message.
4) client receive message.
seL4_Call performance in sel4bench excluding overhead , is it right? = 1) +
2) + 3) + 4) - 3) - 4)
3. This is seL4_Send annotation in benchmark_param.
/* Send slowpath (no fastpath for send) same prio client-server, different
address space */
But client_prio(seL4_MaxPrio - 1) and server_prio(seL4_MaxPrio - 2) is
different.
For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I
have patched seL4 to support for booting from an in-memory execute-in-place
filesystem image that contains the kernel and all user-mode programs
required to mount the root filesystem (similar to that of QNX, but
with more of the
functionality in the bootloader rather than the root server). The existing
seL4 boot process may be OK for static embedded systems that are always
cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with
a boot image that will include files from multiple
separately-installed packages and
will possibly be customized to the system it is installed on.
Requiring any image
filesystem to be linked into the root server makes updating boot images
more complex than being able to use a simple filesystem builder to make an
image containing the kernel, root server, and everything else that is
required (the main special considerations being placing the kernel and root
server at fixed physical addresses and padding the image to allow for bss
sections, which are easy enough). Also, I want it to be easy to manually
boot UX/RT images, so you can just type something like "boot
(hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most
older Unices), and the bootloader will automatically load the kernel and
all required modules from within the image as opposed to having to type a
lot of boilerplate to load the kernel and root server (and anything else
that may be required). In addition I don't think that the root server
should need to have any support for parsing image filesystems and
should be able to obtain all the files required for early boot from
the MBI.
I am using Multiboot2 with a few custom tags added and a few extra
requirements regarding placement of modules. I currently have an
in-memory loader that implements my variant of Multiboot2, and
eventually want to
implement a full disk-based bootloader. I have also implemented a
page-oriented in-memory filesystem called XRFS (originally based on
Linux romfs) with support for placing files at fixed addresses. The
in-memory loader was parsing the filesystem and using a script to
locate the modules within the image, although I have decided that it
is overkill to do that, and it would allow the loader to be simpler if
the filesystem image has its own MBH separate from that of the kernel
(the magic number will be different from the kernel MBH as well), with
tags for the kernel and each module, so that the loader's existing
MBH-parsing code can be used to locate files in the image.
As far as my kernel patches go, they extend the existing Multiboot2
code and do not interfere with the existing boot code. Right now they
are x86-only, but I am planning to add Multiboot2 support to other
architectures eventually as well. They do not introduce any dependency
on my filesystem format in the kernel (it does know that there is an
FS image and that there are modules contained within it, and assumes
that modules are contiguous). Relocation of the root task is disabled
when an FS image is present, since it will already be placed in a
usable location in the image. Kernel-level ELF loading of modules is
also disabled when using my Multiboot2 extensions, since my loader is
capable of parsing ELF modules, loading them, and passing information
on module sections and addresses to the kernel through tags. The part
of the image containing the kernel is inaccessible to the root task
for obvious reasons, so an additional requirement is that the kernel
is the first file in the image, followed by the root server, and then
all other files (XRFS is structured to allow the remainder of the
image to be read even though the beginning is inaccessible). There is
also support for passing the MBI through to the root task, which
requires that the MBI is allocated immediately after the end of the
filesystem image (a new structure is added to the bootinfo to provide
the root server with the address of the MBI).
>From what I've said, would there be any problems with including my
patches in the mainline seL4 repository? Only the boot code is
modified. Loading the root server works, but I haven't yet tested the
MBI passthrough, so I am not quite ready to submit anything (currently
I am working on converting my bootloader from parsing the filesystem
itself to parsing an MBH in the FS image, like I said before).
DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed).
Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released?
Thanks,
Chris Guikema
I am investigating the use of seL4 on heterogeneous architectures such as
the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm
investigating that involves utilising both the Cortex-R5 cores and Core-A53
cores for different applications. I'm rather new to seL4 development so I'm
a bit stuck and need some advice.
It's easiest if I just list my requirements and assumptions for my
architecture design:
a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS
Kernel to manage system resources and run virtual machines.
b) I require the use of the Cortex R5 cores in DCLS mode for trusted code
with high fault tolerance requirements.
c) I require the use of the Cortex A53 cores for running unsafe Linux VMs.
d) It's my understanding that seL4 lacks 64-bit multicore support for its
own scheduler, but VMs running on seL4 could be provided with access to all
the cores? (Eg: Linux)
e) It's my understanding that seL4 lacks heterogeneous task scheduling, and
cannot manage both the Cortex R5 and Cortex A53 cores.
This leads me to make the following architectural conclusions:
[1] It's not possible to boot an seL4 kernel on one processor and have it
manage the other.
[2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and
boot an seL4 kernel on each.
[3] Some domain specific protocol is required for the CPU modules to
communicate and share resources.
Any help or advice would be appreciated.
Regards,
Robbie
Hi all,
I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint?
Best Regards
-Daniel Wang
Hi all
I am new comer to sel4 community. I knew a little bit virtualisation
infrastructe(kvm/qemu), but I know little about sel4/docker.
I am investigating the proper implemenatation for running docker on sel4 on
arm64.
There might several ways I can figure out.Any suggestions are welcome :-)
1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might
be the
easiest way. It might have worked well on X86
2. porting l4linux to sel4. Don't know whether it is feasible?
3. run docker as sel4 service without linux. On this way, golang and its
library should be ported to sel4. Some missed syscalls which are needed by
docker should be implemenated.
Is there any other ways or anything else to make the implatation more
feasible?
---
Cheers,
Justin
HI, I have a question about IPC and SMP.
I ran sel4bench on sabre lite(i.mx6, arm v7).
1. I want to confirm performance difference between Lazy Scheduling and
Beno Scheduling. Can I configure scheduler?
2. Can you explain the difference when thread state is
"ThreadState_Running" and "ThreadState_Restart"?
3. I tried "SMP Benchmark" but I can't understand what this benchmark
exactly means.
What "Cycles" means in this benchmark?
smp : This is an intra-core ipc round-trip benchmark to check overhead of
the kernel synchronization on ipc throughput.
4. I try to measure IPC performance with SMP is on.
I used "seL4_TCB_SetAffinity" function so server executed in Core1 and
client executed Core2.
But performance results are too excessive.
seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles.
Are these results are available?
