AdaCore stärkt mit RecordFlux die Sicherheit binärer Kommunikationsprotokolle
Paris, 28. März 2023 – 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 beweisbarem 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 weniger Aufwand und geringeren 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.
„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.
Weitere Informationen über die RecordFlux-Technologie gibt es auf www.adacore.com/recordflux.
Über AdaCore
AdaCore wurde 1994 gegründet und bietet Tools für Software-Entwicklung und Verifikation für kritische und sicherheitskritische Systeme. Zahlreiche Anwender haben die AdaCore-Produkte im Einsatz und unterhalten damit eine Vielzahl von kritischen Anwendungen in Bereichen wie Raumfahrtsysteme, kommerzielle Luftfahrt, militärische Systeme, im Flugverkehrsmanagement, bei Schienensystemen, bei Geräten der Medizintechnik und bei Finanzdienstleistungen. AdaCore verfügt über eine umfangreiche und wachsende weltweite Kundenbasis; nähere Informationen dazu unter www.adacore.com/customers.
AdaCore-Produkte sind Open-Source und werden mit Online-Support durch die Entwickler zur Verfügung gestellt. Das Unternehmen hat seinen nordamerikanischen Hauptsitz in New York, der europäische Hauptsitz ist in Paris. Weitere Informationen unter www.adacore.com
Pressekontakte
AdaCore
Jessie Glockner
press@AdaCore.com
www.adacore.com
http://twitter.com/AdaCoreCompany
PR-COM GmbH
Andrea Groß
Tel. +49-89-59997-803
andrea.gross@pr-com.de
www.pr-com.de