Crema: Eine Programmiersprache ohne Turing-Vollständigkeit

Um Sicherheitsprobleme zu vermeiden, versucht die Programmiersprache Crema, viele problematische Dinge nicht zuzulassen. Crema verzichtet dabei bewusst auf die sogenannte Turing-Vollständigkeit, um die Analyse des Codes zu erleichtern.

Artikel veröffentlicht am , Hanno Böck
Die Programmiersprache Crema verzichtet bewusst auf die sogenannte Turing-Vollständigkeit.
Die Programmiersprache Crema verzichtet bewusst auf die sogenannte Turing-Vollständigkeit. (Bild: Screenshot Golem.de)

Crema ist eine Programmiersprache, die viele Dinge nicht kann, die in anderen Programmiersprachen selbstverständlich sind. Was zunächst nicht gerade attraktiv klingt, hat seine Gründe: Crema verzichtet auf bestimmte Features, um dabei möglichst sicher zu sein und die formale Analyse des Codes zu erleichtern. Auf der Konferenz Bsides Las Vegas stellte der IT-Sicherheitsforscher Jacob Torrey Crema vor.

Stellenmarkt
  1. Referent (m/w/d) für die Digitalisierung im Rettungsdienst (4. QE)
    Bayerisches Staatsministerium des Innern, für Sport und Integration, München
  2. Fachgruppenleitung Informations- und Kommunikationstechnologien (w/m/d)
    Bundesinstitut für Risikobewertung, Berlin
Detailsuche

Bei Crema handelt es sich um eine Programmiersprache, die nicht Turing-vollständig ist. Die Turing-Vollständigkeit ist ein Konzept aus der theoretischen Informatik und bezieht sich auf das Modell einer Turingmaschine. Praktisch alle gewöhnlichen Programmiersprachen sind Turing-vollständig. Das bedeutet, dass sich - mit der Einschränkung von Speicherverbrauch und Geschwindigkeit - diese Programmiersprachen alle gegenseitig emulieren können.

Halteproblem macht formale Analyse unmöglich

Das Problem: Ein Programm in einer Turing-vollständigen Sprache formal zu analysieren, ist in vielen Fällen unmöglich. Dafür sorgt das sogenannte Halteproblem. Es ist eines der fundamentalen Grundprinzipien der theoretischen Informatik. Demnach lässt sich durch ein anderes Programm nicht zuverlässig entscheiden, ob ein in einer Turing-vollständigen Sprache geschriebenes Programm jemals enden wird. Formale Verifikationssysteme - Torrey erwähnt etwa das Tool KLEE - sind damit grundsätzlich nicht in der Lage, ein in einer Turing-vollständigen Sprache geschriebenes Programm komplett auf bestimmte Fehler zu prüfen.

Konkret bedeutet das, dass in der Programmiersprache Crema endlos laufende Schleifen oder unbeschränkte Rekursionen nicht möglich sind. Crema ist damit für bestimmte Anwendungsfälle nicht geeignet, beispielsweise für Serverdienste, die dauerhaft laufen und auf Verbindungen warten. Auch für Programme mit Benutzerinterface ist Crema generell nicht geeignet. Gedacht ist die Programmiersprache vor allem zur Entwicklung von Parsern für Protokolle und Dateiformate. Gerade hier finden sich meist auch sehr viele Sicherheitslücken - mit fehlerhaften Eingabedaten können Angreifer häufig das Verhalten eines Programms unerwünscht kontrollieren.

Modell der Walther-Rekursion

Golem Akademie
  1. C++ 20: Concepts - Ranges - Coroutinen - Module
    4.-8. Oktober 2021, online
  2. Advanced Python - Fortgeschrittene Programmierthemen
    16./17. September 2021, online
Weitere IT-Trainings

Crema basiert dabei auf einem theoretischen Modell, in dem sich das Programm immer in einem bestimmten Zustand befindet, aber niemals zu einem früheren Zustand zurückkehren kann. Schleifen sind zwar möglich, sie werden aber - zumindest im Modell - in Abhängigkeit der Eingabedaten als separate Codepfade modelliert. Crema folgt dabei einem Konzept namens Walther-Rekursion, ein Modell, das der Darmstädter Informatik-Professor Christoph Walther in den frühen 90ern an der Technischen Universität Darmstadt entwickelt hat.

Crema ist nicht der erste Versuch, eine Programmiersprache ohne Turing-Vollständigkeit zu implementieren. Doch laut Torrey waren die meisten derartigen Versuche bisher äußerst kompliziert zu nutzen und daher für Programmierer unattraktiv. Crema hat Ähnlichkeit mit C und soll möglichst einfach nutzbar sein. Codebeispiele findet man im Wiki von Crema.

Quellcode unter freier Lizenz

Ein wissenschaftliches Hintergrundpaper zu Crema hat Torrey zusammen mit Mark Bridgman im Mai auf dem Langsec-Workshop der IEEE veröffentlicht. Crema nutzt das LLVM-Compiler-Framework und ist selbst in C++ geschrieben. Der Quellcode steht als freie Software unter der MIT-Lizenz auf Github zur Verfügung.

Bitte aktivieren Sie Javascript.
Oder nutzen Sie das Golem-pur-Angebot
und lesen Golem.de
  • ohne Werbung
  • mit ausgeschaltetem Javascript
  • mit RSS-Volltext-Feed


Aktuell auf der Startseite von Golem.de
Hubble
Uralttechnik ohne Ersatz versagt im Orbit

Das Hubble-Teleskop ist außer Betrieb. Die Speicherbänke aus den 1980er Jahren lassen sich nicht mit der CPU von 1974 ansprechen, die auf einer Platine zusammengelötet wurde.
Von Frank Wunderlich-Pfeiffer

Hubble: Uralttechnik ohne Ersatz versagt im Orbit
Artikel
  1. Batteriezellfabrik: Porsche will Hochleistungsakkus mit Silizium-Anoden bauen
    Batteriezellfabrik
    Porsche will Hochleistungsakkus mit Silizium-Anoden bauen

    Akkus für nur 1.000 Elektroautos im Jahr will Porsche mit der neuen Tochterfirma Cellforce bauen. Vor allem für den Motorsport.

  2. Pornografie: Hostprovider soll Xhamster sperren
    Pornografie
    Hostprovider soll Xhamster sperren

    Medienwächter haben den Hostprovider von Xhamster ausfindig gemacht. Dieser soll das Pornoportal für deutsche Nutzer sperren.

  3. SSDs und Monitore zum Knallerpreis beim Amazon Prime Day
     
    SSDs und Monitore zum Knallerpreis beim Amazon Prime Day

    Wer auf der Suche nach neuer Hardware ist, sollte den Prime Day von Amazon nutzen. Hier warten Rabatte auf alle möglichen Artikel.
    Ausgewählte Angebote des E-Commerce-Teams

irata 05. Aug 2015

Soweit schon richtig. Nur Planeten zur Explosion bringen kann man damit nicht. Dafür...

hw75 05. Aug 2015

Der gravierende Unterschied besteht darin, dass nur for-Schleifen möglich sind, aber...

hw75 05. Aug 2015

Der Vorteil ist doch klar beschrieben: man kann ein solches Programm dann vollständig...


Folgen Sie uns
       


Du willst dich mit Golem.de beruflich verändern oder weiterbilden?
Zum Stellenmarkt
Zur Akademie
Zum Coaching
  • Schnäppchen, Rabatte und Top-Angebote
    Die besten Deals des Tages
    Schnäppchen • Amazon Prime Day nur noch heute • SSDs (u. a. Crucial MX500 1TB 75,04€) • Gaming-Monitore • RAM von Crucial • Fire TV Stick 4K 28,99€/Lite 18,99€ • Bosch Professional • Dualsense + Pulse 3D Headset 139,99€ • Gaming-Chairs von Razer uvm. • HyperX Cloud II 51,29€ • iPhone 12 128GB 769€ • TV OLED & QLED [Werbung]
    •  /