Dit artikel is een verzameling nieuwsupdates van Proofcraft uit 2026, waarbij de focus ligt op de formele verificatie van de seL4-microkernel. De belangrijkste technische prestaties zijn:
- Beveiligingsbewijzen: Het voltooien van bewijzen voor vertrouwelijkheid en integriteit op de AArch64-architectuur, wat garandeert dat applicaties veilig geïsoleerd zijn.
- Architectuur-ondersteuning: De MCS-configuratie (voor systemen met gemengde kritikaliteit) is nu geverifieerd voor RISC-V en zal worden geport naar Arm 64-bit.
- Innovaties in Scheduling: De introductie van een dynamische domeinscheduler in seL4 15.0.0, waardoor systemen tijdens runtime kunnen wisselen tussen verschillende timingvereisten (zoals boot- en operationele fasen).
- Academische bijdragen: De presentatie van The Algebra of Iterative Constructions op LICS'26, een theoretisch werk dat bewijsassistenten zoals Isabelle/HOL efficiënter maakt.
Daarnaast reflecteert Proofcraft op hun vijfjarig bestaan en hun betrokkenheid bij diverse conferenties en partnerschappen, waaronder de seL4 summit en projecten gefinancierd door DARPA, NCSC en de Duitse Cyberagentur.
Proofcraft Nieuws - 2026
21 augustus 2026: seL4-beveiligingsbewijzen nu voltooid voor AArch64
Dankzij aanhoudende steun van het NCSC is deze mijlpaal het sluitstuk van het formele bewijs dat de seL4-implementatiecode op AArch64 de beveiligingsisolatie van de applicaties die erop draaien afdwingt (onder de hier vermelde aannames). Deze isolatie voorkomt dat aanvallen op niet-kritieke applicaties overslaan naar kritieke applicaties en deze compromitteren.
24 juli 2026: Proof Engineering en Theorie op LICS'26
Het artikel The Algebra of Iterative Constructions, geschreven door Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat en Todd Schmid, werd deze week gepresenteerd op het 41ste jaarlijkse symposium over logica in de informatica (LICS) in Lissabon.
Dit artikel uit de theoretische informatica gaat over een algebraïsche abstractie en redeneerprincipes voor de iteratieve constructie van vaste punten (fixed points). Vaste punten zijn een terugkerend thema in de informatica met veel bekende resultaten, zoals de stelling van het vaste punt van Kleene. De in dit artikel getoonde algebra maakt het mogelijk om dergelijke stellingen beknopt uit te drukken en enables redeneren op een abstracte en gestroomlijnde manier. Dit kan efficiënt worden geïmplementeerd in bewijsassistenten zoals Isabelle/HOL, wat Proofcraft gebruikt voor de verificatie van de seL4-microkernel.
De hoogautomatische Isabelle/HOL-implementatie van de iteratie-algebra in dit artikel is het resultaat van een spontane samenwerking tussen de Chief Scientist van Proofcraft, Gerwin Klein, en Benjamin Kaminski, die begon tijdens de bijeenkomst van de IFIP Working Group 2.3 (Programming Methodology) in Athene in 2025. Het toont aan dat proof engineering varieert van praktische toepassing tot diepe theorie.
29 juni 2026: MCS seL4 nu geverifieerd (voor RISC-V)
Proofcraft heeft een belangrijke mijlpaal bereikt in de seL4-verificatieroadmap waar jaren aan is gewerkt: de MCS-configuratie van seL4, die ondersteuning biedt voor systemen met gemengde kritikaliteit (mixed-criticality systems), is nu bewezen correct voor RISC-V.
Deze configuratie is de grootste nieuwe seL4-functie en is onmisbaar voor real-time applicaties met gemengde kritikaliteit, zoals automotive use cases. Het bevat uitgebreide wijzigingen in de implementatie en API van de kernel. De verificatie hiervan vereiste daarom aanzienlijke inspanningen en was al lange tijd een prioriteit in de seL4-roadmap.
Proofcraft heeft nu, voor het eerst, de verificatie van de functionele correctheid voor seL4 met MCS voltooid. Functionele correctheid is het grootste en meest centrale bewijs in de seL4-verificatiestack. Het bewijs is gericht op de RISC-V-architectuur en zal nu worden geport naar de Arm 64-bit-architectuur, als onderdeel van het PROVERS-programma van DARPA.
1 juni 2026: Dynamische domeinscheduler voor seL4
Proofcraft heeft de implementatie en het formele bewijs geleverd van een flexibelere domeinscheduling in seL4.
Vóór deze wijziging vereisten de seL4-beveiligingsbewijzen, en in het bijzonder het bewijs van de handhaving van informatiestromen, een volledig statische planning die in de kernel was gecompileerd. Dit betekende dat wanneer seL4 werd gebruikt om de grenzen van informatiestromen tussen applicaties af te dwingen, ontwikkelaars een vaste, vooraf bepaalde hoeveelheid tijd per domein moesten opgeven voor de gehele levensduur van het draaiende systeem. Dit strikte beleid maakte het moeilijk om informatiestroombeheer in de praktijk toe te passen en te ondersteunen in SDK-stijl ontwikkeling, zoals de Microkit.
Proofcraft stelde een nieuwe seL4 runtime API (Application Programming Interface) voor die het laden van semi-statische domeinschemas mogelijk maakt. Dit betekent dat een systeem met informatiestroombescherming tijdens de runtime verschillende fasen kan doorlopen die voldoen aan verschillende timingvereisten voor domeinen. Bijvoorbeeld:
- Bootfase: Kan langere tijdslots hebben om virtuele machines te laten starten zonder hun domeintijdtoewijzing te overschrijden.
- Operationele fase: Kan kortere tijdslots bieden, zodat elk domein responsief is voor externe interactie.
Daarnaast kan een SDK-gebaseerd systeem, zoals de Microkit, de nieuwe API gebruiken om tijdens het opstarten een domeinschema in te stellen. Deze nieuwe seL4 API is geïmplementeerd, geverifieerd en beschikbaar in seL4 15.0.0.
21 mei 2026: Keynote van June Andronick op de CDIS-voorjaarsconferentie in Stockholm
Op 21 mei 2026 hield CDIS – het Zweedse onderzoekscentrum voor cyberdefensie en informatiebeveiliging – zijn voorjaarsconferentie aan het KTH Royal Institute of Technology in Stockholm.
CEO van Proofcraft, June Andronick, was een van de twee keynote-sprekers, samen met August Martens van Mistral AI. June gaf een overzicht van formele verificatie voor cybersecurity en nam deel aan een panel over digitale soevereiniteit.
28 april 2026: Proofcraft presenteert op de Cyberagentur Milestone Research summit
In april 2026 organiseerde de Duitse Cyberagentur een Milestone Research summit om de voortgang en resultaten van haar gefinancierde programma's te presenteren, waaronder het onderzoeksprogramma Ecosystem trustworthy IT (ÖvIT), waarvan Proofcraft een ontvanger is in partnerschap met Kry10.
De Chief Scientist van Proofcraft, Gerwin, en de Chief Scientist van Kry10, Martin Dehnel-Wild, presenteerden de voortgang van het Dyvercon-project, dat dynamiek, prestaties en bewijzen moet leveren voor complexe cyber-fysische systemen. In het bijzonder rapporteerde Gerwin over het werk van Proofcraft aan het uitbreiden van de seL4-bewijzen ter ondersteuning van een statische multikernel-configuratie. Hierbij kunnen applicaties profiteren van het gebruik van meerdere CPU-cores voor prestaties, terwijl er op kernniveau een aparte instantie van seL4 op elke core draait.
Daarnaast gaf Gerwin een algemene introductie tot formele verificatie en een overzicht van het gebruik ervan in de echte wereld.
17 april 2026: Proofcraft is trots sponsor van de seL4 summit 2026
Proofcraft ondersteunt de seL4 summit van 2026 als Silver-sponsor. De seL4 summit is een jaarlijkse internationale bijeenkomst van deelnemers uit de industrie, overheid en universiteiten met interesse in de meest hoogwaardig verzekerde OS-kernel ter wereld. Deelnemers en presentatoren zijn onder meer de makers en beheerders van de seL4-technologie, zoals het Proofcraft-team.
De seL4 summit van dit jaar vindt plaats in Vancouver, Canada, van 1 tot 3 september 2026.
14 april 2026: 5 jaar Proofcraft: 5 jaar dichter bij een geverifieerde toekomst
Op 14 april 2021 hebben we Proofcraft opgericht. Vijf jaar later zijn we zo druk bezig met het werken aan een geverifieerde toekomst dat we een tijdje geen nieuws hebben geplaatst. Er is veel gebeurd en er komt meer aan. Hier zijn enkele technische hoogtepunten die Proofcraft heeft geleverd:
- Arm-ondersteuning: De seL4-bewijzen worden nu ondersteund op 100% van de Arm-platforms waarop de kernel kan draaien. Hiermee wordt de afhankelijkheid van experts verminderd en kunnen gebruikers van seL4 vrij kiezen tussen de ondersteunde Arm-platforms met de zekerheid dat ze een geverifieerde codebase gebruiken. Dit werk is onderdeel van het PROVERS-programma van DARPA.
- Integriteit op AArch64: seL4 op AArch64 dwingt nu bewijsbaar integriteit af. We hebben een formeel wiskundig bewijs dat de kernel voorkomt dat een applicatie die bovenop seL4 draait, ongeautoriseerd gegevens wijzigt.
- Beveiligingsbewijzen: Het werk aan beveiligingstheorema's gaat door. Dankzij aanhoudende steun van het NCSC zijn we dicht bij het voltooien van de vertrouwelijkheidseigenschap, en daarmee de volledige beveiligingsbewijsstack voor de 64-bit Arm-architectuur.
Er gebeurt veel meer, met drie grote projecten die parallel lopen, respectievelijk gefinancierd door DARPA, Cyberagentur en NCSC. Blijf op de hoogte!
Proofcraft Nieuws - 2026
21 augustus 2026: seL4-beveiligingsbewijzen nu voltooid voor AArch64
Dankzij aanhoudende steun van het NCSC is deze mijlpaal het sluitstuk van het formele bewijs dat de seL4-implementatiecode op AArch64 de beveiligingsisolatie van de applicaties die erop draaien afdwingt (onder de hier vermelde aannames). Deze isolatie voorkomt dat aanvallen op niet-kritieke applicaties overslaan naar kritieke applicaties en deze compromitteren.
24 juli 2026: Proof Engineering en Theorie op LICS'26
Het artikel The Algebra of Iterative Constructions, geschreven door Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat en Todd Schmid, werd deze week gepresenteerd op het 41ste jaarlijkse symposium over logica in de informatica (LICS) in Lissabon.
Dit artikel uit de theoretische informatica gaat over een algebraïsche abstractie en redeneerprincipes voor de iteratieve constructie van vaste punten (fixed points). Vaste punten zijn een terugkerend thema in de informatica met veel bekende resultaten, zoals de stelling van het vaste punt van Kleene. De in dit artikel getoonde algebra maakt het mogelijk om dergelijke stellingen beknopt uit te drukken en enables redeneren op een abstracte en gestroomlijnde manier. Dit kan efficiënt worden geïmplementeerd in bewijsassistenten zoals Isabelle/HOL, wat Proofcraft gebruikt voor de verificatie van de seL4-microkernel.
De hoogautomatische Isabelle/HOL-implementatie van de iteratie-algebra in dit artikel is het resultaat van een spontane samenwerking tussen de Chief Scientist van Proofcraft, Gerwin Klein, en Benjamin Kaminski, die begon tijdens de bijeenkomst van de IFIP Working Group 2.3 (Programming Methodology) in Athene in 2025. Het toont aan dat proof engineering varieert van praktische toepassing tot diepe theorie.
29 juni 2026: MCS seL4 nu geverifieerd (voor RISC-V)
Proofcraft heeft een belangrijke mijlpaal bereikt in de seL4-verificatieroadmap waar jaren aan is gewerkt: de MCS-configuratie van seL4, die ondersteuning biedt voor systemen met gemengde kritikaliteit (mixed-criticality systems), is nu bewezen correct voor RISC-V.
Deze configuratie is de grootste nieuwe seL4-functie en is onmisbaar voor real-time applicaties met gemengde kritikaliteit, zoals automotive use cases. Het bevat uitgebreide wijzigingen in de implementatie en API van de kernel. De verificatie hiervan vereiste daarom aanzienlijke inspanningen en was al lange tijd een prioriteit in de seL4-roadmap.
Proofcraft heeft nu, voor het eerst, de verificatie van de functionele correctheid voor seL4 met MCS voltooid. Functionele correctheid is het grootste en meest centrale bewijs in de seL4-verificatiestack. Het bewijs is gericht op de RISC-V-architectuur en zal nu worden geport naar de Arm 64-bit-architectuur, als onderdeel van het PROVERS-programma van DARPA.
1 juni 2026: Dynamische domeinscheduler voor seL4
Proofcraft heeft de implementatie en het formele bewijs geleverd van een flexibelere domeinscheduling in seL4.
Vóór deze wijziging vereisten de seL4-beveiligingsbewijzen, en in het bijzonder het bewijs van de handhaving van informatiestromen, een volledig statische planning die in de kernel was gecompileerd. Dit betekende dat wanneer seL4 werd gebruikt om de grenzen van informatiestromen tussen applicaties af te dwingen, ontwikkelaars een vaste, vooraf bepaalde hoeveelheid tijd per domein moesten opgeven voor de gehele levensduur van het draaiende systeem. Dit strikte beleid maakte het moeilijk om informatiestroombeheer in de praktijk toe te passen en te ondersteunen in SDK-stijl ontwikkeling, zoals de Microkit.
Proofcraft stelde een nieuwe seL4 runtime API (Application Programming Interface) voor die het laden van semi-statische domeinschemas mogelijk maakt. Dit betekent dat een systeem met informatiestroombescherming tijdens de runtime verschillende fasen kan doorlopen die voldoen aan verschillende timingvereisten voor domeinen. Bijvoorbeeld:
- Bootfase: Kan langere tijdslots hebben om virtuele machines te laten starten zonder hun domeintijdtoewijzing te overschrijden.
- Operationele fase: Kan kortere tijdslots bieden, zodat elk domein responsief is voor externe interactie.
Daarnaast kan een SDK-gebaseerd systeem, zoals de Microkit, de nieuwe API gebruiken om tijdens het opstarten een domeinschema in te stellen. Deze nieuwe seL4 API is geïmplementeerd, geverifieerd en beschikbaar in seL4 15.0.0.
21 mei 2026: Keynote van June Andronick op de CDIS-voorjaarsconferentie in Stockholm
Op 21 mei 2026 hield CDIS – het Zweedse onderzoekscentrum voor cyberdefensie en informatiebeveiliging – zijn voorjaarsconferentie aan het KTH Royal Institute of Technology in Stockholm.
CEO van Proofcraft, June Andronick, was een van de twee keynote-sprekers, samen met August Martens van Mistral AI. June gaf een overzicht van formele verificatie voor cybersecurity en nam deel aan een panel over digitale soevereiniteit.
28 april 2026: Proofcraft presenteert op de Cyberagentur Milestone Research summit
In april 2026 organiseerde de Duitse Cyberagentur een Milestone Research summit om de voortgang en resultaten van haar gefinancierde programma's te presenteren, waaronder het onderzoeksprogramma Ecosystem trustworthy IT (ÖvIT), waarvan Proofcraft een ontvanger is in partnerschap met Kry10.
De Chief Scientist van Proofcraft, Gerwin, en de Chief Scientist van Kry10, Martin Dehnel-Wild, presenteerden de voortgang van het Dyvercon-project, dat dynamiek, prestaties en bewijzen moet leveren voor complexe cyber-fysische systemen. In het bijzonder rapporteerde Gerwin over het werk van Proofcraft aan het uitbreiden van de seL4-bewijzen ter ondersteuning van een statische multikernel-configuratie. Hierbij kunnen applicaties profiteren van het gebruik van meerdere CPU-cores voor prestaties, terwijl er op kernniveau een aparte instantie van seL4 op elke core draait.
Daarnaast gaf Gerwin een algemene introductie tot formele verificatie en een overzicht van het gebruik ervan in de echte wereld.
17 april 2026: Proofcraft is trots sponsor van de seL4 summit 2026
Proofcraft ondersteunt de seL4 summit van 2026 als Silver-sponsor. De seL4 summit is een jaarlijkse internationale bijeenkomst van deelnemers uit de industrie, overheid en universiteiten met interesse in de meest hoogwaardig verzekerde OS-kernel ter wereld. Deelnemers en presentatoren zijn onder meer de makers en beheerders van de seL4-technologie, zoals het Proofcraft-team.
De seL4 summit van dit jaar vindt plaats in Vancouver, Canada, van 1 tot 3 september 2026.
14 april 2026: 5 jaar Proofcraft: 5 jaar dichter bij een geverifieerde toekomst
Op 14 april 2021 hebben we Proofcraft opgericht. Vijf jaar later zijn we zo druk bezig met het werken aan een geverifieerde toekomst dat we een tijdje geen nieuws hebben geplaatst. Er is veel gebeurd en er komt meer aan. Hier zijn enkele technische hoogtepunten die Proofcraft heeft geleverd:
- Arm-ondersteuning: De seL4-bewijzen worden nu ondersteund op 100% van de Arm-platforms waarop de kernel kan draaien. Hiermee wordt de afhankelijkheid van experts verminderd en kunnen gebruikers van seL4 vrij kiezen tussen de ondersteunde Arm-platforms met de zekerheid dat ze een geverifieerde codebase gebruiken. Dit werk is onderdeel van het PROVERS-programma van DARPA.
- Integriteit op AArch64: seL4 op AArch64 dwingt nu bewijsbaar integriteit af. We hebben een formeel wiskundig bewijs dat de kernel voorkomt dat een applicatie die bovenop seL4 draait, ongeautoriseerd gegevens wijzigt.
- Beveiligingsbewijzen: Het werk aan beveiligingstheorema's gaat door. Dankzij aanhoudende steun van het NCSC zijn we dicht bij het voltooien van de vertrouwelijkheidseigenschap, en daarmee de volledige beveiligingsbewijsstack voor de 64-bit Arm-architectuur.
Er gebeurt veel meer, met drie grote projecten die parallel lopen, respectievelijk gefinancierd door DARPA, Cyberagentur en NCSC. Blijf op de hoogte!
Groetjes,