A platform-evidence mapping for DAL-B certification planning on an AMD64 multi-core processor with Xen temporal isolation

Moderne vliegtuigen worden steeds complexer en vertrouwen op krachtige computers om alles te beheren, van vluchtcontroles tot navigatie en missieplanning. Om de veiligheid te waarborgen, gebruikt de luchtvaartindustrie strikte regels die vereisen dat elke software wordt getest en geverifieerd tot een specifiek betrouwbaarheidsniveau. Voor de meest kritieke systemen, zoals die welke een vliegtuig in de lucht houden, is dit betrouwbaarheidsniveau het hoogst mogelijke. Echter, een nieuwe uitdaging is ontstaan naarmate deze computers zijn geëvolueerd van enkele processoren naar multi-core chips, vergelijkbaar met de krachtige processors die in moderne laptops en servers worden gevonden. Wanneer meerdere programma's tegelijkertijd draaien op verschillende kernen van dezelfde chip, concurreren ze vaak om toegang tot gedeelde bronnen, specifiek een hoogwaardig geheugengebied dat de last-level cache wordt genoemd. Deze concurrentie kan ervoor zorgen dat één programma onvoorspelbaar vertraagt, wat een onzekerheid in de timing creëert die gevaarlijk is voor veiligheidskritische luchtvaartsoftware.

Om dit op te lossen, ontwikkelen onderzoekers manieren om deze programma's te isoleren zodat ze elkaar niet hinderen. Een veelbelovende aanpak omvat een type softwarebeheerder, een hypervisor genoemd, die tussen de hardware en de applicaties zit en de computerbronnen verdeelt in afzonderlijke, beveiligde compartimenten. De vraag blijft echter of deze isolatie sterk genoeg is om te voldoen aan de strenge normen die vereist zijn voor de commerciële luchtvaart. Een team onderzoekers van Advanced Micro Devices en de Technische Universiteit München heeft deze vraag verkend door een gedetailleerd plan op te stellen voor hoe een specifiek type multi-core computer te certificeren voor gebruik in vliegtuigen. Hun werk richt zich op een configuratie die een hypervisor genaamd Xen op AMD-processors gebruikt, gecombineerd met een techniek genaamd cache coloring, om ervoor te zorgen dat verschillende softwarepartities niet per ongeluk op elkaars tenen kunnen trappen.

De onderzoekers begonnen met het identificeren van het specifieke probleem: op een multi-core processor is de gedeelde geheugencache de primaire plek waar interferentie plaatsvindt. Als één programma de cache vult, kan dit een ander programma dwingen te wachten, wat vertragingen veroorzaakt waardoor kritieke deadlines mogelijk worden gemist. Om dit te voorkomen, stelde het team een methode voor waarbij het geheugen van de computer wordt verdeeld in afzonderlijke groepen, of "kleuren", gebaseerd op waar de data zich bevindt. Elk softwareprogramma krijgt zijn eigen unieke set kleuren toegewezen, en het systeem wordt zo geconfigureerd dat data van het ene programma nooit de data van het andere programma kan vervangen in de cache. Cruciaal is dat deze regel ook geldt voor de hypervisor zelf. De onderzoekers hebben ervoor gezorgnd dat de eigen data van de softwarebeheerder ook wordt vergrendeld in zijn eigen exclusieve kleurengroep, wat voorkomt dat het per ongeluk de data van de veiligheidskritieke programma's die het beheert, verdringt. Dit creëert een constructieve garantie dat de interferentie begrensd is, wat betekent dat het wiskundig beperkt en voorspelbaar is, in plaats van er alleen maar op te hopen dat het niet gebeurt.

Het artikel presenteert een mapping van deze technische opstelling naar de officiële certificeringsregels die worden gebruikt door luchtvaartautoriteiten in de Verenigde Staten en Europa. Deze regels, bekend als DO-178C en AC 20-193, vereisen dat aanvragers bewijzen dat gedeelde bronnen veilig worden beheerd. De auteurs demonstreren hoe hun specifieke configuratie aan deze vereisten voldoet door aan te tonen dat het cache coloring-mechanisme de last-level cache effectief isoleert. Ze laten ook zien hoe de eigen safety case van de hypervisor, die apart door de open-source community wordt gedocumenteerd, kan worden hergebruikt als bewijs voor de vliegtuigfabrikant. Hierdoor kan de fabrikant zich concentreren op het bewijzen dat hun specifieke applicaties correct werken binnen deze geïsoleerde omgeving, in plaats van dat zij de onderliggende computerhardware vanaf nul moeten bewijzen. De onderzoekers schetsen een duidelijk pad voor hoe een vliegtuigfabrikant deze opstelling kan gebruiken om een middelmatig veiligheidsniveau te bereiken, bekend als DAL-B, dat geschikt is voor veel belangrijke maar niet levenskritieke functies.

De auteurs zijn echter voorzichtig met het definiëren van de grenzen van hun werk. Ze stellen expliciet dat dit plan nog niet bewijst dat het systeem veilig genoeg is voor het absoluut hoogste niveau van certificering, bekend als DAL-A, dat vereist is voor de meest kritieke vluchtcontroles. Om dat hogere niveau te bereiken, zouden aanvullende stappen nodig zijn, zoals het formeel bewijzen met wiskunde dat de geheugentoewijkingstool nooit een fout maakt en het verzamelen van meer uitgebreide praktijkervaring met de specifieke processor. Het artikel verduidelijkt ook dat het geen AI-workloads of grafische verwerking behandelt, wat opkomende gebieden zijn die verschillende oplossingen vereisen. Bovendien benadrukken de auteurs dat dit een methodologiepapier is, geen definitieve certificering; het biedt een gestructureerd argument en een reeks instrumenten, maar de werkelijke goedkeuring moet nog steeds komen van de luchtvaartinstanties die de specifieke details van elk vliegtuigprogramma zullen beoordelen.

De kern van het onderzoek is een praktische demonstratie van hoe deze abstracte veiligheidsregels kunnen worden toegepast op een echt computingplatform. Het team beschreef een specifieke configuratie waarbij een computer met vier kernen wordt verdeeld in aparte partities voor verschillende taken, zoals vluchtbesturing, perceptie en missiebeheer. Ze lieten zien hoe elke partitie een toegewezen kern en een specifieke slice van de geheugencache kan krijgen, waardoor wordt gegarandeerd dat de vluchtbesturingssoftware altijd over de middelen beschikt die zij nodig heeft zonder dat zij wordt vertraagd door de andere taken. Ze beschreven ook hoe het systeem bij het opstarten op fouten controleert om te verzekeren dat de geheugenisolatie correct werkt voordat het vliegtuig ooit opstijgt. Deze aanpak biedt een manier om krachtige, commercieel beschikbare computerchips te gebruiken in de luchtvaart zonder de voorspelbaarheid en veiligheid op te offeren die de industrie eist.

Uiteindelijk biedt het artikel een brug tussen de snelle evolutie van commerciële computerhardware en het trage, bedachtzame tempo van veiligheidscertificering in de luchtvaart. Het laat zien dat het met de juiste configuratie, specifiek door gebruik te maken van cache coloring en een statische partitionerende hypervisor, mogelijk is om een computingomgeving te creëren waarin interferentie gecontroleerd en voorspelbaar is. Hoewel de weg naar de hoogste niveaus van certificering nog werk vereist, biedt dit onderzoek een solide fundament voor fabrikanten om te beginnen met de integratie van deze geavanceerde processors in hun vliegtuigen. Het werk dient als een blauwdruk en demonstreert dat de technische mechanismen bestaan om veilige multi-core integratie te ondersteunen, mits de specifieke regels en bewijzen die door toezichthouders worden vereist, zorgvuldig worden gevolgd en geverifieerd.