Hoe betrouwbaar is onze software?
Van vertrouwen naar bewijs
Software is uitgegroeid van ondersteunend hulpmiddel tot kritieke infrastructuur. In een wereld van geopolitieke spanningen, digitale afhankelijkheid en toenemende systeemcomplexiteit wordt betrouwbaarheid een strategische factor. Volgens Marieke Huisman, hoogleraar Software Reliability aan de Universiteit Twente, is het tijd voor een omslag: van impliciet vertrouwen naar aantoonbaar bewijs.
Tekst: Cees Visser Beeld: AJF
Onze maatschappij draait op software’, stelt Huisman. ‘Van financiële systemen tot energievoorziening: alles is digitaal.’ Software is daarmee niet langer alleen een technisch vraagstuk, maar ook een geopolitieke factor. Europa is in hoge mate afhankelijk van buitenlandse technologie, met name van Amerikaanse cloud- en platformleveranciers. Die afhankelijkheid beperkt de controle over data en systemen en brengt risico’s met zich mee voor digitale soevereiniteit. Softwareketens zijn bovendien internationaal en complex, waardoor organisaties beperkt zicht hebben op de herkomst en werking van componenten. Zolang systemen functioneren, blijft die afhankelijkheid grotendeels onzichtbaar — tot het misgaat. Volgens Huisman zou het helpen als kritieke software, zoals systemen rond DigiD, vaker opensource beschikbaar is. ‘Dan kan een brede groep experts meekijken en fouten sneller aan het licht brengen.’ Hoewel organisaties daar terughoudend in zijn, kan meer transparantie volgens haar juist bijdragen aan betere softwarekwaliteit.
Huisman wijst erop dat afhankelijkheden ook een strategische dimensie hebben. Moderne systemen, inclusief defensietoepassingen, zijn in sterke mate softwaregedreven. ‘Dat onderstreept hoe belangrijk het is om te begrijpen en te beheersen hoe software zich gedraagt, zeker wanneer die afkomstig is uit internationale ketens’, aldus de hoogleraar.
‘Het is noodzakelijk om niet minder, maar juist méér te verifiëren’
Tegelijkertijd is het maatschappelijke besef van deze afhankelijkheid beperkt. Software is zo diep verankerd in het dagelijks leven dat ze grotendeels onzichtbaar blijft. Juist in tijden van internationale spanningen krijgt die afhankelijkheid extra gewicht. De kwetsbaarheid neemt verder toe door de groeiende complexiteit van software. Moderne systemen bestaan uit miljoenen regels code en zijn opgebouwd uit externe libraries, api’s en diensten. Volledige controle is daardoor nauwelijks haalbaar.
Nieuwe ontwikkelingen versterken dat effect. De opkomst van ai-gegenereerde code versnelt softwareontwikkeling, maar vermindert vaak het inzicht in de werking ervan. Ontwikkelaars vertrouwen steeds vaker op automatisch gegenereerde code zonder die volledig te doorgronden. Dat leidt tot software die wel functioneert, maar waarvan het gedrag niet altijd volledig begrepen wordt. Juist in die context neemt het belang van verificatie toe. Huisman: ‘Het is noodzakelijk om niet minder, maar juist méér te verifiëren: als software essentieel is, moet aantoonbaar zijn wat systemen doen.’
Wiskundige modellen
De technieken om software systematisch te controleren zijn niet nieuw; de eerste ideeën stammen uit de jaren zestig en zeventig. Formele methoden maken gebruik van wiskundige modellen om eigenschappen van software te bewijzen, bijvoorbeeld door gewenst gedrag exact te specificeren of alle mogelijke toestanden van een systeem te analyseren. In theorie bieden deze technieken krachtige mogelijkheden om fouten vroegtijdig op te sporen. In de praktijk blijft toepassing echter achter. Volgens Huisman ligt dat niet aan de effectiviteit, maar aan de toegankelijkheid. ‘De methoden zijn complex en vereisen specialistische kennis, wat voor veel ontwikkelteams een drempel vormt. Daarnaast spelen tijdsdruk en kosten een rol: verificatie wordt nog vaak gezien als extra stap, terwijl de baten zich later uitbetalen.’
Dat leidt tot een klassiek spanningsveld tussen korte- en langetermijnbelangen. Onder druk van deadlines en budgetten krijgen snelheid en functionaliteit vaak prioriteit boven zekerheid. Toch is de economische logica volgens Huisman helder: fouten die laat worden ontdekt, zijn aanzienlijk duurder om te herstellen. In kritische systemen kunnen ze bovendien leiden tot verstoringen, beveiligingsincidenten en reputatieschade. De waarde van verificatie zit juist in het voorkomen van problemen.
‘Programmeertalen, frameworks en ontwikkelmethoden veranderen snel, waardoor onderzoek zich continu moet aanpassen’
VerCors
Om de kloof tussen theorie en praktijk te verkleinen, werkt Huisman met haar onderzoeksgroep aan VerCors (Verification of Concurrent Software), een verificatietool die sinds 2011 in ontwikkeling is. ‘Het doel is formele methoden toegankelijk te maken voor reguliere ontwikkelaars. De tool analyseert broncode en controleert of die voldoet aan gespecificeerde eigenschappen, zodat fouten vroeg zichtbaar worden. Ontwikkelaars krijgen directe feedback over mogelijke problemen en oplossingen.’ De ontwikkeling van dergelijke tools blijft volgens haar echter een uitdaging. Programmeertalen, frameworks en ontwikkelmethoden veranderen snel, waardoor onderzoek zich continu moet aanpassen. Het doel is verificatie zo te integreren in bestaande workflows dat het net zo vanzelfsprekend wordt als testen of code review.
Perspectief
In de loop van haar carrière heeft Huisman haar perspectief op softwareverificatie zien verschuiven. Waar ze aanvankelijk uitging van volledig bewezen, foutloze software, erkent ze dat volledige zekerheid in de praktijk zelden haalbaar is. De complexiteit en schaal van moderne systemen maken sluitend bewijs vrijwel onmogelijk. Dat maakt verificatie echter niet minder relevant. Het doel verschuift naar aantoonbare kwaliteitsverbetering en het zo vroeg mogelijk opsporen van fouten, zegt ze daarover.
Betrouwbaarheid en veiligheid zijn daarbij nauw verweven. Softwarefouten vormen vaak de basis voor beveiligingslekken, variërend van onbedoelde datatoegang tot exploiteerbare kwetsbaarheden. Volgens Huisman ontstaan deze risico’s vaak doordat het gedrag van software niet expliciet wordt vastgelegd en gecontroleerd. Verificatietechnieken kunnen helpen om die eigenschappen inzichtelijk te maken en te borgen. Veiligheid moet daarom geen sluitpost zijn, maar een integraal onderdeel van ontwerp en ontwikkeling.
‘Besluitvorming over digitale systemen vindt niet altijd plaats met voldoende technische kennis’
Kloof
Er bestaat nog altijd een kloof tussen academisch onderzoek en de praktijk. Universiteiten richten zich op fundamentele inzichten en publicaties, terwijl bedrijven behoefte hebben aan direct toepasbare oplossingen. Ook binnen de academie speelt een spanningsveld: promovendi moeten publiceren, terwijl het ontwikkelen van bruikbare tools andere prioriteiten vraagt. Voor implementatie zijn vaak aanvullende rollen nodig, gericht op engineering en productontwikkeling.
Tegelijkertijd ziet Huisman dat bedrijven zich meer en meer bewust zijn van het belang van softwarekwaliteit. De uitdaging ligt in het aantonen van de meerwaarde en het praktisch toepasbaar maken van technieken. Ook bij de overheid is ruimte voor verbetering. Besluitvorming over digitale systemen vindt niet altijd plaats met voldoende technische kennis, terwijl de impact groot is. Volgens Huisman vraagt dat om meer inhoudelijke expertise bij beleidsmakers.
Geen enkele partij kan dit vraagstuk alleen oplossen. Bedrijven brengen praktijkervaring, de wetenschap methodologische kennis en de overheid sturingskracht. Juist de combinatie daarvan is nodig om softwarebetrouwbaarheid structureel te verbeteren.
Studenten
Onderwijs speelt hierin een belangrijke rol. Studenten leren niet alleen programmeren, maar vooral hoe ze software bouwen die begrijpelijk en controleerbaar is. Het gaat niet om de hoeveelheid code, maar om de kwaliteit en de verantwoording ervan. Daarmee ontstaat een nieuwe generatie ontwikkelaars die betrouwbaarheid als uitgangspunt neemt.
De conclusie: in een samenleving waarin software de ruggengraat vormt van vrijwel alle processen, volstaat impliciet vertrouwen niet langer. Systemen worden complexer, afhankelijkheden nemen toe en de impact van fouten groeit. Organisaties moeten daarom toewerken naar aantoonbare controle over hun software. Zekerheid zal nooit absoluut zijn, maar met betere methoden, tooling en samenwerking kan de betrouwbaarheid aanzienlijk worden vergroot.
Of zoals Huisman het samenvat: ‘We moeten van vertrouwen naar bewijs. Alleen dan houden we grip op de systemen die ons dagelijks leven bepalen.’
Voor de liefhebber
Hoe werkt VerCors in de praktijk? In dit voorbeeld ziet VerCors dat de implementatie iets anders doet dan de specificatie zegt. Klik hier voor het voorbeeld.
Marieke Huisman is hoogleraar Software Reliability aan de Universiteit Twente. Haar onderzoek richt zich op formele methoden voor softwareverificatie en het vroegtijdig opsporen van fouten in complexe systemen. Zij leidt de ontwikkeling van de verificatietool VerCors en werkt op het snijvlak van theorie en praktijk.
