Hacker News Reader

Comment by TeMPOraL | Hacker News Reader

Security.

A lot of security vulnerabilities in programs essentially boil down to your code being an ad-hoc parser for an (often implicit) language that's more powerful than you wanted. Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it.

This is a very insightful way of looking at things, and is a research area called langsec.

See:

- http://langsec.org/

- Papers and public talks of Meredith L. Patterson

- https://www.gwern.net/Turing-complete for some examples of unexpected Turing-completeness

View on HN

> Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it.

Can I ask why Turing-completeness is "especially dangerous"?

Let's say we have a pure language for e.g. generating a JSON value (nested lists/maps of strings, floats, nulls and booleans). It has no primitives other than null, true/false, string, float, list, map and function literals, and corresponding "arithmetic" functions for each type.

What would the safety and security differences be between such a language being Turing-complete and not being Turing-complete?

Programs in these languages can't "do" anything, other than calculate. The only problem I can think of is making denial-of-service easier, by e.g. generating an infinitely large list and running out of memory:

    (\x -> [ null ] ++ (x x)) (\x -> [ null ] ++ (x x))

This will generate `[ null, null, null, ... ]` until it runs out of memory. However, we could still blow the memory without Turing-completeness, e.g. by growing an exponentially large datastructure for a large number of steps (basically like a zip bomb):

    (\f xs -> case xs of
                   nil         -> [ null ]
                   (cons y ys) -> (f f ys) ++ (f f ys))
    (\f xs -> case xs of
                   nil         -> [ null ]
                   (cons y ys) -> (f f ys) ++ (f f ys))
    [ null, null, null, null, null, ...and so on 1000 times ]

This recursion is well-founded, and structurally-decreasing since we only call `f` with a strictly-decreasing value of `xs`, until we hit the base-case for `xs = nil` where we return `[ null ]`. In the non-base-case we recurse twice to generate two identical lists, then append them together. This results in a list with 2^1000 elements, easily consuming all available memory.

Hence for security, we need to kill programs which go over some predefined time/memory bounds regardless of whether or not they're Turing-complete. Hence my question about whether or not Turing-completeness is "especially dangerous", in comparison to e.g. I/O primitives.

The latter example you gave will still not type-check in Dhall, although I'll still answer the spirit of your question

You can write expressions in Dhall that will take a long time to evaluate (see the Ackerman example elsewhere in this thread), but it's harder to do so by accident. Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them

> Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them

Don't get me wrong, I'm all in favour of totality! My question was mostly about the "especially dangerous" wording. In my opinion, the major advantage of using Dhall for config instead of say, Scheme, is that it's pure/referentially-transparent/has-no-IO/etc., which everyone seems to be ignoring in favour of debating whether or not totality is desirable

(Of course, Dhall does have "I" (but not "O") in the form of imports, but these are "morally pure" as long as URL contents are stable, similar to Nix's imports being "morally pure" as long as builds are deterministic).

> The latter example you gave will still not type-check in Dhall

Incidentally, how does Dhall check for totality? I know it's based on the calculus of constructions; does it use syntactic guardedness checks like Coq?

Whilst I like totality, I'm still undecided about whether it's worth enforcing in general-purpose languages (e.g. Agda, rather than Dhall), since totality checking is still quite restrictive. The usability balance for static typing was crossed by Hindley-Milner, but I'm yet to see such an unobtrusive approach to totality checking (whenever my Coq or Agda projects become more than toys, they tend to get wrapped up in a monadic `Delay` to avoid fighting things like syntactic guardedness!)

Dhall does the dumbest thing possible to enforce totality: Dhall doesn't support recursion! Note that Dhall does support lists and folds on lists (which are total), but not user-defined recursion

For example, if you write:

    let x = x in x

... then the second `x` will be flagged as an unbound variable because `let`-bound variables are not in scope for their own definitions. Similarly, there is no `let rec` in Dhall

That implies that if you want a user-defined recursive type that was not a list then you have to explicitly Boehm-Berarducci-encode the recursive type and its inhabitants. For example, if you wanted to encode the following Haskell data type in your configuration:

    data Tree = Node Integer | Branch Tree Tree

    example :: Tree
    example = Branch (Node 1) (Branch (Node 2) (Node 3))

... you would encode it like this:

        λ(Tree : Type)
    →   λ(Branch : Tree → Tree → Tree)
    →   λ(Node : Integer → Tree)
    →   Branch (Node 1) (Branch (Node 2) (Node 3))

You can think of Boehm-Berarducci encoding as "anonymous recursion" when you write it this way because every inhabitant of such a "recursive" type includes the datatype definition in the value (if you view the lambda-bound type and constructors as the datatype definition)

Or to put it another way, if you ignore Dhall's support for builtin types, builtin functions, and imports then Dhall is literally the exact same thing as System Fw . You're used to thinking of System Fw or the calculus of constructions as underlying core languages for a higher-level language semantically defined in terms of the core language like Coq, Agda or Haskell. However, in Dhall there is no underlying core language: you are assembling raw System Fw expressions. Since the most pedantic definition of System Fw requires explicit polymorphism and doesn't support recursion then Dhall behaves the same way, too.

I agree, though, that the lack of (unsafe) IO is an even bigger deal. Like you mentioned, if you use immutable URLS (such as IPFS) then they are basically pure. Even if you do use mutable URLs, you can always use the ability to normalize programs to purify them of imports (and you can also use Dhall's API to safely and statically verify that an expression is devoid of imports).

Reply on news.ycombinator.com