{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/nl\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic ontwikkelt technieken voor formele verificatie van bestaande software met behulp van AI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Het bedrijf Anthropic heeft de resultaten gepresenteerd van experimenten met AI-modellen voor formele verificatie van de betrouwbaarheid en veiligheid van bestaande projecten. Tijdens het experiment werden met behulp van AI-modellen wiskundige bewijzen gegenereerd voor 123 open bibliotheken, getest in de OSS Fuzz-infrastructuur, om aan te tonen dat er geen geheugenfouten optraden. <\/p>\n
De controle werd uitgevoerd op het niveau van gecompileerde assemblycode voor de RISC-V-architectuur. Het totale volume van de gegenereerde bewijzen bedroeg ongeveer 180 miljoen regels code voor het verificatiesysteem Rocq Prover (ongeveer 600.000 regels per binaire bestand met 18.000 RISC-V-instructies). De bewijzen werden gegenereerd door bestaande fuzzing-tests automatisch om te zetten naar formele specificaties, waarna het AI-model Claude bewees dat de applicatie, ongeacht de invoer tot 64 MB, geen fouten vertoonde. <\/p>\n
Tijdens het opbouwen van de bewijzen kon het AI-model honderden fouten identificeren en voorbereidende correcties aanbrengen die eerder niet opgemerkt waren tijdens fuzzing-tests. Onder andere werden kwetsbaarheden ontdekt die leidden tot buffer-overflows bij het verwerken van bepaalde invoerdata (zoals CVE-2026-56132 in libexpat), evenals logische fouten. Daarnaast werd het AI-model gebruikt om de naleving van de implementatie van het zlib-algoritme in de Linux-kernel aan de RFC 1950-specificatie te bewijzen.<\/p>\n
Ook werd er een interpreter in Rust gegenereerd voor een subset van de taal Python, waarvoor met behulp van de Verus-tooling een formeel bewijs van overeenkomst met de semantiek van CPython werd voorbereid. Voor het vergelijken van het gedrag met CPython werden meer dan 1,7 miljoen willekeurig gegenereerde Python-programma's uitgevoerd. In 99,95% van de gevallen kwamen de uitvoeringsresultaten van deze programma's in de nieuwe implementatie en in CPython overeen, terwijl de ontdekte discrepanties bekende randgevallen waren.<\/p>\n
De uitgevoerde formele verificatie garandeert de naleving van de specificatie, maar sluit niet volledig de mogelijkheid van beveiligingsproblemen uit, aangezien de risico's die voortkomen uit multithreading, dynamisch linken en abnormaal gedrag van echt hardware niet formeel zijn vastgelegd. Een belangrijk voordeel van de voorgestelde aanpak is het werken met binaire bestanden, wat het mogelijk maakt om de noodzaak van het herschrijven van bestaande code in formeel verifieerbare talen te omzeilen. \n Bron: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"