Code maken zonder lekken door wiskundige verificatie

Het schrijven van geverifieerd veilige code

Karthik Bhargavan:…bewezen veilig …

Programmeren is mensenwerk, maar de wiskunde is onverslaanbaar. Als je het programmeren wiskundiger zou maken zou je daarmee voorkomen dat er fouten in de code sluipen die kunnen worden misbruikt door e-krakers en veiligheidsdiensten, denken informatici. Een stap in die richting is de manier waarop de kryptobieb EverCrypt is ontwikkeld. De onderzoekers die daaraan gewerkt hebben konden bewijzen dat hun code geheel ongevoelig is voor de belangrijkste webaanvallen die in het verleden slachtoffers hebben gemaakt. “Als we zeggen bewijs dan bedoelen we dat onze code geen last heeft van zulke aanvallen”, zegt Karthik Bhargavan, een informaticus die in Parijs bij Inria werkt. Dat zou moeten smaken naar meer. Lees verder

Kraakbestendige code door wiskundig programmeren

Wiskundig programmeren, afb Boya SunNu steeds vaker allerlei digitale inbraken en overvallen worden gemeld, gecombineerd met de nog steeds toenemende digitalisering van de maatschappij doet zich de vraag voor hoe we van die ellende af kunnen komen. Dat schijnt te kunnen stelt het Amerikaanse  Quanta Magazine, met wat zij ‘formele verificatie’ noemt; een programmeermethode die sluitend is als een wiskundig bewijs en ik daarom aanduid met wiskundige programmeren. Die programmeerwijze zou foutloze programmatuur opleveren. E-krakers en ander digitaal geboefte maken meestal juist gebruik van fouten in de code. Die gaan moeilijke tijden tegemoet Lees verder