7 ms·

Crema: A Sub-Turing Programming Language

29 points by omnibrain 11y ago

dgreensp 11y ago
There's no clear value proposition given. What are we sacrificing Turing-completeness in order to gain? For example, one thing a programming language might gain by sacrificing Turing-completeness is that every program provably halts; no infinite loops! This is called "total function programming." There are probably other interesting properties you can gain by sacrificing Turing-completeness as well. Crema can restrict the computational complexity of the program to the minimum needed to improve security "Computational complexity" is a technical term that is related to performance, but not security.
- sirseal 11y ago
  From the Crema wiki that I just glanced at, it is indeed not possible to write infinite loops: "The only type of loop supported by Crema is the foreach loop. This loop is used to sequentially iterate over each element of a list. Crema specifically does not support other common loops (such as while or for loops) so that Crema programs are forced to operate in sub-Turing Complete space. In other words, foreach loops always have a defined upper bound on the number of iterations possible during the loop's execution. This makes it impossible to write a loop that could execute for an arbitrary length of time."
- samuell 11y ago
  Well, from my understanding, I would say "security" is a very broad term, being influenced by a broad range of factors including "computational complexity", don't you think?
- GFK_of_xmaspast 11y ago
  If all you're doing is sacrificing the possibility for infinite loops, just hack a c++ runtime that kills a process after 24 hours, and blammo non-Turing complete.
- DenisM 11y ago
  This is called "total function programming." Thanks for bringing it up, I was not aware of this: https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming Recently I had a need to design a small language for a constrained environment, and I spent a bit of time worrying about termination problem. Now I know where to look for more research.
- otabdeveloper 11y ago
  > There are probably other interesting properties you can gain by sacrificing Turing-completeness as well. Not the author, but I wrote another sub-Turing language. In my opinion, there's two useful properties: a) type inference -- you can infer the type of the whole program b) you can infer memory use and thus avoid the need for garbage collection or manual memory management. Both properties are very useful for performance, of course. :)
  - Ono-Sendai 11y ago
    Hi, I'm writing a total functional language as well. I think that garbage collection is still useful however, as it can collect garbage as the program runs, not just at the end.
    - otabdeveloper 11y ago
      I've managed to make it so my memory use is completely deterministic -- no garbage at all.
      - Ono-Sendai 11y ago
        That sounds interesting. Any references or notes on that I can read? (or source code :) ) I would say that just because your memory use is deterministic, doesn't mean you don't get garbage. Garbage is just memory that isn't needed any more. for example, in let a = f(x) b = g(y) in a + b If there is working memory used in the body of f(), it will be garbage when f() has finished executing, because it won't be referred to any more. So it could be freed after f is executed and before g is executed, which may reduce the maximum amount of memory required by the program.
capitalsigma 11y ago
Do they forbid recursion? I don't see anything about it on the wiki, but I assume they must.
- Ono-Sendai 11y ago
  not necessarily, you can bound recursion.
- swolchok 11y ago
  crema/tests/fail/ includes several tests relating to recursion, including the obvious mutual recursion workaround attempt. Given that they're in the fail subdirectory, I conclude that it's testing that they're rejected.
- tromp 11y ago
  Presumably you can only call functions defined earlier.
schoen 11y ago
This is comparable to a more practically usable version of Douglas Hofstadter's BlooP. https://en.wikipedia.org/wiki/BlooP_and_FlooP https://en.wikipedia.org/wiki/BlooP_and_FlooP The inspiration for claiming this more restricted language is a security benefit comes directly from Sassaman, Patterson, Bratus, and Shubina: http://langsec.org/papers/Sassaman.pdf http://langsec.org/papers/Sassaman.pdf (See "Principle 1". "Computational power is an important and heretofore neglected dimension of the attack surface. Avoid exposing unnecessary computational power to the attacker. An input language should only be as computationally complex as absolutely needed, so that the computational power of the parser necessary for it can be minimized. For example, if recursive data structures are not needed, they should not be specified in the input language.") Further research on these ideas has continued under the name of the "language-theoretic security research program". http://www.langsec.org/ http://www.langsec.org/ This language is surely intended as a contribution to that project. (The behavior of programs in Crema, as in BlooP, is decidable, which should help with correctness verification.)
- qznc 11y ago
  Are there also language-based approaches to defend against timing attacks? Are there languages which zero buffers/variables after use?
  - schoen 11y ago
    I don't think those topics have been addressed in LANGSEC (although it might be easier to examine all the possible timing properties of code in a non-Turing-complete environment). An approach to the second topic is described in https://www.usenix.org/legacy/event/sec05/tech/full_papers/chow/chow.pdf https://www.usenix.org/legacy/event/sec05/tech/full_papers/c...
    - qznc 11y ago
      Thanks! The paper is interesting, but not language-based. They change runtime (more precisely libc-free) and kernel. I was thinking about something different. In C++ you could create a wrapper type (similar to smart pointers) which zeros on deallocation. However, there is the problem that the compiler could optimize the zeros away, because nobody reads those writes. So you really need language/compiler support to do this correctly and future-proof.
black_knight 11y ago
As I understand it, Crema's fixed length loops gives it the computation power of primitive recursive functions. Which is enough for most programming applications. However, that assumes that a program is something which runs, computes a result and is done. A lot of programs fall outside that scope — even if they do not require more computational complexity per se. A daemon or an operating system are typical examples of programs without bounded computation times. Not because of their computational complexity, but because they continuously (or by demand) produce new results. The interesting property for them is not termination, but productivity. They must keep being productive, and not become unresponsive. This is much more subtle notion than termination, but I think the programming language Agda has come some way with its co-recursive data types.
tromp 11y ago
Instead of Crema's int i = 0 int values[] = [6, 3, 8, 7, 2, 1, 4, 9, 0, 5] foreach (values as dummy) { int_print(values[i]) i = i + 1 } it would be more straightforward to define loops over array indexing ranges, as in foreach (int i indexing values) { int_print(values[i]) }
- adrusi 11y ago
  It would seem that you could implement that abstraction within the language def int int_indexing(int values[])[] { int i = 0 int result[] = list_create(list_length(values)) foreach (values as dummy) { result[i] = i i = i + 1 } return result } I haven't tested this, and I had to look in the source code to find the list_create function from the standard library. Of course, since the language lacks type parameterization, you'd need a different indexing function for each type of array.
otabdeveloper 11y ago
Cool! Another sub-Turing language is my own 'tab', (https://bitbucket.org/tkatchev/tab https://bitbucket.org/tkatchev/tab), a text processing language/utility. 'Tab' was born out of a practical need to process text files in a manner similar to SQL statements, so the focus is different from research languages. Hope the trend catches on, sub-Turing languages are cool.

29 points by omnibrain 11y ago

There's no clear value proposition given. What are we sacrificing Turing-completeness in order to gain? For example, one thing a programming language might gain by sacrificing Turing-completeness is that every program provably halts; no infinite loops! This is called "total function programming." There are probably other interesting properties you can gain by sacrificing Turing-completeness as well. Crema can restrict the computational complexity of the program to the minimum needed to improve security "Computational complexity" is a technical term that is related to performance, but not security.

sirseal 11y ago
From the Crema wiki that I just glanced at, it is indeed not possible to write infinite loops: "The only type of loop supported by Crema is the foreach loop. This loop is used to sequentially iterate over each element of a list. Crema specifically does not support other common loops (such as while or for loops) so that Crema programs are forced to operate in sub-Turing Complete space. In other words, foreach loops always have a defined upper bound on the number of iterations possible during the loop's execution. This makes it impossible to write a loop that could execute for an arbitrary length of time."
samuell 11y ago
Well, from my understanding, I would say "security" is a very broad term, being influenced by a broad range of factors including "computational complexity", don't you think?
GFK_of_xmaspast 11y ago
If all you're doing is sacrificing the possibility for infinite loops, just hack a c++ runtime that kills a process after 24 hours, and blammo non-Turing complete.
DenisM 11y ago
This is called "total function programming." Thanks for bringing it up, I was not aware of this: https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming Recently I had a need to design a small language for a constrained environment, and I spent a bit of time worrying about termination problem. Now I know where to look for more research.
otabdeveloper 11y ago
> There are probably other interesting properties you can gain by sacrificing Turing-completeness as well. Not the author, but I wrote another sub-Turing language. In my opinion, there's two useful properties: a) type inference -- you can infer the type of the whole program b) you can infer memory use and thus avoid the need for garbage collection or manual memory management. Both properties are very useful for performance, of course. :)
- Ono-Sendai 11y ago
  Hi, I'm writing a total functional language as well. I think that garbage collection is still useful however, as it can collect garbage as the program runs, not just at the end.
  - otabdeveloper 11y ago
    I've managed to make it so my memory use is completely deterministic -- no garbage at all.
    - Ono-Sendai 11y ago
      That sounds interesting. Any references or notes on that I can read? (or source code :) ) I would say that just because your memory use is deterministic, doesn't mean you don't get garbage. Garbage is just memory that isn't needed any more. for example, in let a = f(x) b = g(y) in a + b If there is working memory used in the body of f(), it will be garbage when f() has finished executing, because it won't be referred to any more. So it could be freed after f is executed and before g is executed, which may reduce the maximum amount of memory required by the program.

capitalsigma 11y ago

Do they forbid recursion? I don't see anything about it on the wiki, but I assume they must.

Ono-Sendai 11y ago
not necessarily, you can bound recursion.
swolchok 11y ago
crema/tests/fail/ includes several tests relating to recursion, including the obvious mutual recursion workaround attempt. Given that they're in the fail subdirectory, I conclude that it's testing that they're rejected.
tromp 11y ago
Presumably you can only call functions defined earlier.

schoen 11y ago

This is comparable to a more practically usable version of Douglas Hofstadter's BlooP. https://en.wikipedia.org/wiki/BlooP_and_FlooP https://en.wikipedia.org/wiki/BlooP_and_FlooP The inspiration for claiming this more restricted language is a security benefit comes directly from Sassaman, Patterson, Bratus, and Shubina: http://langsec.org/papers/Sassaman.pdf http://langsec.org/papers/Sassaman.pdf (See "Principle 1". "Computational power is an important and heretofore neglected dimension of the attack surface. Avoid exposing unnecessary computational power to the attacker. An input language should only be as computationally complex as absolutely needed, so that the computational power of the parser necessary for it can be minimized. For example, if recursive data structures are not needed, they should not be specified in the input language.") Further research on these ideas has continued under the name of the "language-theoretic security research program". http://www.langsec.org/ http://www.langsec.org/ This language is surely intended as a contribution to that project. (The behavior of programs in Crema, as in BlooP, is decidable, which should help with correctness verification.)

qznc 11y ago
Are there also language-based approaches to defend against timing attacks? Are there languages which zero buffers/variables after use?
- schoen 11y ago
  I don't think those topics have been addressed in LANGSEC (although it might be easier to examine all the possible timing properties of code in a non-Turing-complete environment). An approach to the second topic is described in https://www.usenix.org/legacy/event/sec05/tech/full_papers/chow/chow.pdf https://www.usenix.org/legacy/event/sec05/tech/full_papers/c...
  - qznc 11y ago
    Thanks! The paper is interesting, but not language-based. They change runtime (more precisely libc-free) and kernel. I was thinking about something different. In C++ you could create a wrapper type (similar to smart pointers) which zeros on deallocation. However, there is the problem that the compiler could optimize the zeros away, because nobody reads those writes. So you really need language/compiler support to do this correctly and future-proof.

black_knight 11y ago

As I understand it, Crema's fixed length loops gives it the computation power of primitive recursive functions. Which is enough for most programming applications. However, that assumes that a program is something which runs, computes a result and is done. A lot of programs fall outside that scope — even if they do not require more computational complexity per se. A daemon or an operating system are typical examples of programs without bounded computation times. Not because of their computational complexity, but because they continuously (or by demand) produce new results. The interesting property for them is not termination, but productivity. They must keep being productive, and not become unresponsive. This is much more subtle notion than termination, but I think the programming language Agda has come some way with its co-recursive data types.

tromp 11y ago

Instead of Crema's int i = 0 int values[] = [6, 3, 8, 7, 2, 1, 4, 9, 0, 5] foreach (values as dummy) { int_print(values[i]) i = i + 1 } it would be more straightforward to define loops over array indexing ranges, as in foreach (int i indexing values) { int_print(values[i]) }

adrusi 11y ago
It would seem that you could implement that abstraction within the language def int int_indexing(int values[])[] { int i = 0 int result[] = list_create(list_length(values)) foreach (values as dummy) { result[i] = i i = i + 1 } return result } I haven't tested this, and I had to look in the source code to find the list_create function from the standard library. Of course, since the language lacks type parameterization, you'd need a different indexing function for each type of array.

otabdeveloper 11y ago

Cool! Another sub-Turing language is my own 'tab', (https://bitbucket.org/tkatchev/tab https://bitbucket.org/tkatchev/tab), a text processing language/utility. 'Tab' was born out of a practical need to process text files in a manner similar to SQL statements, so the focus is different from research languages. Hope the trend catches on, sub-Turing languages are cool.