AdaCore, Anbieter von Softwareentwicklungs- und Verifikationswerkzeugen für geschäfts- und sicherheitskritische Systeme, veröffentlicht RecordFlux. Das neue Toolset ermöglicht die Implementierung hochsicherer binärer Kommunikationsprotokolle.
RecordFlux umfasst unter anderem eine domänenspezifische Sprache (DSL) zur präzisen Beschreibung komplexer binärer Datenformate und Kommunikationsprotokolle. Außerdem sind Werkzeuge für die formale Verifikation von Spezifikationen und zur Generierung von mathematisch beweisbaren SPARK-Code enthalten, der nativ ausgeführt werden kann.
Mit RecordFlux können Benutzer komplexe Kommunikationsprotokolle definieren und implementieren sowie Sicherheitseigenschaften wie Speichersicherheit mit deutlich geringerem Aufwand und Kosten garantieren, als es mit einem manuellen Ansatz möglich wäre. Die Präzision der RecordFlux-DSL stellt sicher, dass die erstellten Spezifikationen eindeutig sind. Ihre Ausdrucksstärke macht sie für Domänenexperten leicht verständlich und erlaubt es, auch komplexeste Protokolle zu formalisieren. Der Codegenerator von RecordFlux erzeugt Quellcode in der formal verifizierbaren Sprache SPARK, der automatisch bewiesen werden kann. Dadurch wird eine ganze Bandbreite von Sicherheitseigenschaften garantiert, was sicheren und zuverlässigen Code zu geringeren Kosten ermöglicht.
"Mit RecordFlux bieten wir eine Lösung, die Zeit und Geld spart, indem sie die Generierung von beweisbarem Code automatisiert. Gleichzeitig stellt sie sicher, dass angreifbare Schwachstellen wie Pufferüberläufe von vornherein vermieden werden"
„Die Interaktion zwischen Softwarekomponenten wird durch Protokoll- und Formatspezifikationen definiert. Leider sind die meisten Spezifikationen komplexe, in englischer Sprache verfasste Texte, die manuell in Software übersetzt werden müssen. Dieser Ansatz lässt viel Raum für Fehler“, erklärt Alex Senier, RecordFlux Team Lead bei AdaCore. „Logikfehler und kritische Schwachstellen werden durch die weit verbreitete Verwendung unsicherer Programmiersprachen oft nur unzureichend verhindert, was zu schwerwiegenden Sicherheitslücken führt. Mit RecordFlux bieten wir eine Lösung, die Zeit und Geld spart, indem sie die Generierung von beweisbarem Code automatisiert. Gleichzeitig stellt sie sicher, dass angreifbare Schwachstellen wie Pufferüberläufe von vornherein vermieden werden.“
Über RecordFlux
RecordFlux ist ein Toolset zur Erstellung hochsicherer Implementierungen von binären Datenformaten und Kommunikationsprotokollen. Die Technologie umfasst eine domänenspezifische Sprache, ein umfassendes Toolset und maßgeschneiderte Unterstützung durch Experten. Die Verwendung von SPARK Pro ermöglicht es Entwicklern, den aus RecordFlux-Spezifikationen generierten SPARK-Code automatisch daraufhin zu überprüfen, ob er frei von Laufzeitfehlern ist und der ursprünglichen Spezifikation entspricht.
Der von RecordFlux erzeugte Code ist auch mit GNAT Pro Assurance kompatibel, der Komplettlösung von AdaCore für Projekte mit den strengsten Anforderungen an Zuverlässigkeit, langfristige Wartbarkeit oder Zertifizierung. Die von GNAT Pro Assurance bereitgestellten Compiler-Hardening-Optionen können genutzt werden, um das Risiko von Angriffen auf netzwerkorientierten, protokollverarbeitenden Code weiter zu reduzieren.