Abo
  • Services:
Anzeige
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: Eine Programmiersprache ohne Turing-Vollständigkeit

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)

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.

Anzeige

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.

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

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.


eye home zur Startseite
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...



Anzeige

Stellenmarkt
  1. über Hanseatisches Personalkontor Mannheim, Mannheim
  2. LEDVANCE GmbH, Garching bei München
  3. Sagemcom Fröschl GmbH, Walderbach (zwischen Cham und Regensburg)
  4. Jobware Online-Service GmbH, Paderborn


Anzeige
Blu-ray-Angebote
  1. (u. a. The Big Bang Theory, The Vampire Diaries, True Detective)
  2. (u. a. The Revenant, Batman v Superman, James Bond Spectre, Legend of Tarzan)
  3. (u. a. Hobbit Trilogie Blu-ray 43,89€ und Batman Dark Knight Trilogy Blu-ray 17,99€)

Folgen Sie uns
       


  1. Digital Paper DPT-RP1

    Sonys neuer E-Paper-Notizblock wird 700 US-Dollar kosten

  2. USB Typ C Alternate Mode

    Thunderbolt-3-Docks von Belkin und Elgato ab Juni

  3. Sphero Lightning McQueen

    Erst macht es Brummbrumm, dann verdreht es die Augen

  4. VLC, Kodi, Popcorn Time

    Mediaplayer können über Untertitel gehackt werden

  5. Engine

    Unity bekommt 400 Millionen US-Dollar Investorengeld

  6. Neuauflage

    Neues Nokia 3310 soll bei Defekt komplett ersetzt werden

  7. Surface Studio

    Microsofts Grafikerstation kommt nach Deutschland

  8. Polar

    Fitnesstracker A370 mit Tiefschlaf- und Pulsmessung

  9. Schutz

    Amazon rechtfertigt Sperrungen von Marketplace-Händlern

  10. CPU-Architektur

    RISC-V-Patches für Linux erstmals eingereicht



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
The Surge im Test: Frust und Feiern in der Zukunft
The Surge im Test
Frust und Feiern in der Zukunft
  1. Computerspiele und Psyche Wie Computerspieler zu Süchtigen erklärt werden sollen
  2. Wirtschaftssimulation Pizza Connection 3 wird gebacken
  3. Mobile-Games-Auslese Untote Rundfahrt und mobiles Seemannsgarn

Redmond Campus Building 87: Microsofts Area 51 für Hardware
Redmond Campus Building 87
Microsofts Area 51 für Hardware
  1. Windows on ARM Microsoft erklärt den kommenden x86-Emulator im Detail
  2. Azure Microsoft betreut MySQL und PostgreSQL in der Cloud
  3. Microsoft Azure bekommt eine beeindruckend beängstigende Video-API

3D-Druck bei der Bahn: Mal eben einen Kleiderhaken für 80 Euro drucken
3D-Druck bei der Bahn
Mal eben einen Kleiderhaken für 80 Euro drucken
  1. Bahnchef Richard Lutz Künftig "kein Ticket mehr für die Bahn" notwendig
  2. Flatrate Öffentliches Fahrradleihen kostet 50 Euro im Jahr
  3. Nextbike Berlins neues Fahrradverleihsystem startet

  1. Re: Warum überhaupt VLC nutzen

    __destruct() | 14:46

  2. Re: 300¤

    El Gato | 14:34

  3. Re: Gutes Konzept... schrottiges OS, und dann 4000¤

    Seroy | 14:28

  4. Re: Ich werd es mir wohl kaufen oder gibt es...

    picaschaf | 14:19

  5. Re: 700$ - Ich hätte da eine bessere Lösung...

    picaschaf | 14:19


  1. 10:10

  2. 09:59

  3. 09:00

  4. 18:58

  5. 18:20

  6. 17:59

  7. 17:44

  8. 17:20


  1. Themen
  2. A
  3. B
  4. C
  5. D
  6. E
  7. F
  8. G
  9. H
  10. I
  11. J
  12. K
  13. L
  14. M
  15. N
  16. O
  17. P
  18. Q
  19. R
  20. S
  21. T
  22. U
  23. V
  24. W
  25. X
  26. Y
  27. Z
  28. #
 
    •  / 
    Zum Artikel