Syslog

Show Notes and Links Michael Roitzsch returns to Syslog and we talk about scheduling in operating systems. Michael has focussed his research on soft real-time systems and explored, among other things, how good scheduling can help with smooth video display. In this episode, we introduce basic scheduling concepts, what is happening in scheduling today and how the increasingly multi-core world will shape schedulers in the future. Michael is the acting head of the TU Dresden Operating Systems group and researcher at the Barkhausen Institute. Additional sound effects from https://www.zapsplat.com. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources GWU Lecture: Linux CFS vs Real-Time Scheduling TU Dresden: Operating Systems Group Syslog: Contact Tracing Apps Wikipedia: Real-time Computing ATLAS Arachne Grand Central Dispatch (GCD)

Show Notes and Links Werner Haas, resident hardware expert and colleague at Cyberus Technology, joins Flo and Julian to talk about the state of processor hardware in 2020. We discuss instruction set archicture (ISA) in the context of the x86 vs. ARM vs. RISC-V debate and why CPU ISA might not be that important for performance and battery life after all. Additional sound effects from https://www.zapsplat.com. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter.

Show Notes and Links In this episode, we talk with Martin Decky about HelenOS. HelenOS is a modular multiserver operating system based on a custom microkernel. It has been implemented by a group of people at the Charles University in Prague and is unusual for being a non-commercial operating system project with such a long history. It is fair to say that Martin has shaped HelenOS and HelenOS has shaped Martin for almost the last two decades. Join us while we cover the beginnings of HelenOS, its design philosophy and its struggles over its long lifetime. Additional sound effects from https://www.zapsplat.com. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources MS-DOS Turbo Pascal Not Invented Here HelenOS Project HelenOS Source Code HelenOS precompiled boot images Martin’s PhD thesis, describing design principles of HelenOS List of open source microkernel projects (maintained by Jakub Jermar) Department of Distributed and Dependable Systems at Charles University Operating Systems course at Charles University Abstraction Inversion Anti-Pattern

Show Notes and Links Flo and Julian managed to get Marius Melzer into the recording studio and talk with him about his passion: Formal Verification. In this episode, we make a broader sweep compared to our earlier spotlight on Ada/SPARK and touch on many projects that are on-going in the formal verification community. We discuss how to get going with formal verification and also touch on the theoretical underpinnings. We forgot to mention it in the episode, but please also check out Marius’ other project: palava.tv! Additional sound effects from https://www.zapsplat.com. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources Erlang Elixir Haskell Haskell Programming from First Principles Lambda Days Coq seL4 DeepSpec Project Everest Idris Ada/SPARK Isabelle Lean Frama-C LiquidHaskell F*

Show Notes and Links Flo and Julian invited Jo Van Bulck to the Syslog Podcast. Jo is probably best known for discovering the Foreshadow vulnerability in Intel CPUs, but his research is into the broader security of Trusted Execution Environments (TEEs). In this episode, we’ve picked the most high-profile TEE technology: Jo guides us through the confusing and impressive thing that is the Intel Software Guard Extensions. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources Intel SGX Whitepaper SGX 101 Foreshadow Foreshadow Scientific Paper Plundervolt Load Value Injection Zombieload Overview of Transient Execution Attacks SGX-Step SGX-Step Tutorial Nemesis: Studying Microarchitectural Timing Leaks in Rudimentary CPU Interrupt Logic A Tale of Two Worlds: Assessing the Vulnerability of Enclave Shielding Runtimes Sancus

Show Notes and Links Flo and Julian talk with Michael Hohmuth, who is the head and co-founder of Kernkonzept. Michael was already interested in operating systems before he joined the OS group at TU Dresden. He started to write the first L4 variant in a high-level language when the state of the art was to write them in assembly. Many years later, Michael together with other long-time L4 developers continue their passion at Kernkonzept. We talk with Michael about how L4 began and evolved in Dresden, how work continues at Kernkonzept and how L4 eventually powered a smart oven (among other things, of course). Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources L4 Microkernel Family The Performance of µ-Kernel-based Systems The Nizza Secure-System Architecture Genua L4Re Kernkonzept Kernkonzept Github ELAN programming language SOSP Conference SiMKo 3 phone Elektrobit Rob Pike: Systems Software Research is Irrelevant Singularity OS Fuchsia OSDev Wiki

Show Notes and Links Flo and Julian talk with Michael Roitzsch who is the acting head of the Chair of Operating Systems at our alma mater and researcher at the Barkhausen Institute. Michael currently participates in the PEPP-PT project and shares his insights on the technical and political challenges surrounding SARS-CoV-2 contact tracing apps. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources Barkhausen Institute PEPP-PT (Pan-European Privacy-Preserving Proximity Tracing) dontkillmyapp.com Apple/Google Alliance DP-3T PACT Covidsafe TCN Coalition Need to Know

Show Notes and Links Flo and Julian talk with Michael Engel who went from teaching operating systems fundamentals in Germany to researching sustainability at the NTNU in Norway. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources Dirty ships Plea for a Holistic Analysis of the Relationship between Information Technology and Carbon-Dioxide Emissions emscripten Fabrice Bellard’s x86 emulator written in JavaScript Purism, makers of the Librem laptops and the [Librem 5 phone](https://puri.sm/products/librem-5/ Openmoko Michael Engel’s blog Project Oberon: The Design of an Operating System and Compiler by Niklaus Wirth Plea for Lean Software by Niklaus Wirth School of Niklaus Wirth Computer Latency 1977-2007 Oberon FPGA-system DIGITAL FX!32:Combining Emulation and Binary Translation

Show Notes and Links Flo and Julian talk with Norman Feske, one of the founders of Genode Labs, about how to turn an idea into a company. We touch on operating system research, the Genode OS Framework, and Sculpt OS. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. FOSDEM 2020 Talks Demonstration of the Sculpt Operating System Spunky: a Genode Kernel in Ada/SPARK A Brief Survey through Genode’s ARMv8 Playground Resources Genode OS Project Genode Labs Sculpt OS Genodians Blog Genode Subreddit Genode Book MNT Reform (DIY Laptop)

Show Notes and Links Flo and Julian talk to Alexander Senier about Ada, SPARK and how to build reliable and trustworthy software. We also talk about Alexander’s company, Componolit. Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter. Resources to get started awesome Ada: A curated list of awesome resources related to the Ada and SPARK programming language. learn.adacore.com Free book: Safe and Secure Software - An invitation to Ada 2012 Implementation Guidance for the Adoption of SPARK John W. McCormick, Peter C. Chapin: Building High Integrity Applications with SPARK Ada for the C++ or Java Developer Rust and SPARK: Reliability for Everyone (the statements on SPARK pointers are outdated!) Alire: the Ada package manager Ada Devevelopers room at FOSDEM Low-level and systems programming resources Ada Bare Bones Spunky: A kernel using Ada Ada drivers library Ada Operating System development example Resources specific to component-based systems Genode has built-in support for SPARK/Ada Muen, a separation kernel fully implemented in SPARK Ewok, a microkernel for embedded systems implemented in SPARK Gneiss - framework for platform-independent SPARK components running on Genode, Muen and Linux RecordFlux - Verifiable message parser/generators in SPARK Article: SPARK as an extremum: Components in pure SPARK

Show Notes and Links Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly. Send feedback to podcast@ukvly.org or via Twitter.