5 ms·

> What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages a

by pron 9y ago

> What we can do, and often do is to reduce the practical problems of working on these systems by lifting subsets of problems out of general purpose languages and into much weaker special purpose environments. A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email. It's not a question of general-purpose vs. DSL. Regardless of what the language is for, with no loop, subroutines and variables there is very little you can do. > I've repeatedly pointed out that the entire goal of these languages is to prevent* general reasoning. That is a feature, not a flaw. It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible. For example, regular expressions do not allow "arbitrary computation" in the Turing completeness sense, yet it is infeasible to feasibly answer arbitrary questions about arbitrary regular expressions, such as the question "are two regular expressions equivalent?" This is a very important question about regular expressions, but it cannot be feasibly answered for arbitrary regular expressions.

vidarh 9y ago
> A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email. Most extensions to Sieve still retain the same constraints. A few don't, sometimes because peoples needs are different: E.g. someone using it for their own mail server or a corporate mail server where it is possible to yell at the person who turned their mail script into a fork bomb has very different requirements from one that lets "anyone" sign up, for example. That's a good reason for why the extension mechanism is there. As for examples of other things you can do: There are a number of templating languages, for example, that can be demonstrated to always terminate and otherwise be feasible to reason about. I've personally written such template engines also because it was a useful way of preventing the developers from doing stupid things (the ingrates then tried to sneak in a directive to embed a perl interpreter behind my back at one point). You can do a lot more than you might think in such engines by e.g. providing primitives for filtering and iteration over nodes in input graphs (as long as you can't mutate the collections, and there are appropriate termination guarantees e.g. by preventing loops) Another highly useful example that springs to mind is BPF, which while it started as a basic packet filter (e.g. for tcpdump) is increasingly powering much more functionality on Linux for e.g. tracing, and such as for example kernel level enforcement of system call constraints (you can define filters to apply to subsequent code that e.g. outright rejects certain system calls, or applies comparisons to the system call arguments to decide whether to allow or reject them). But I'd say the question you're asking is the wrong one, though. The original point was that when approaching a problem, there is substantial value to be had by asking "how can I subdivide this problem so that as much as possible can be restricted to a less powerful subset?" The Rule of Least Power, basically. Often you will end up with dynamic subsets that are hard to reason about, but as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest. You don't even need to create full blown languages to get this effect - changing the way you write code and effectively create a DSL in the form of API's can often achieve the same effect, but isolating "dangerous" functionality to separate languages often makes it harder to violate the requirements. > It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible That'd be reasonable apart for setting it up for a No True Scotsman with your "assuming it's useful enough etc.". As we've seen with your objections to Sieve, the languages I'm talking about appears to be languages you don't find "useful enough." Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.
- pron 9y ago
  > as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest. Alas, this was proven wrong for verification in 2005. See https://pron.github.io/posts/correctness-and-complexity#correctness-does-not-decompose https://pron.github.io/posts/correctness-and-complexity#corr... > Since your objections applies to a different set of languages than those I'm talking about, your objections are moot. 1. I reject your examples on the ground that they're considered insufficient for their own domains, and in any case are so restricted that you could not compose the lion share of an application from them even without the theorem showing that you cannot reduce the cost of composition by verifying simple components. 2. While I'm happy to further ponder the utility of the languages you listed, you should bear in mind that, say, a Java program using similar constructs to a Sieve program can be reasoned about automatically by current tools, and with relative ease. In other words, a program so simple is easy to reason about whether it's written in a restricted or a non-restricted language, so using those DSLs just increases the cost of verification. However, that does not mean they are not useful. For example, I read that the main design object of Sieve is to allow servers to run untrusted code.

by pron 9y ago

vidarh 9y ago

> A language that has no variables, no loops and no subroutines (and no regexps) is as far as you can go while remaining feasibly verifiable. There aren't many other options. What portion of our applications can be written in such languages? That people add extensions to Sieve only shows that its trusted portion isn't widely-enough useful even for the task of filtering email. Most extensions to Sieve still retain the same constraints. A few don't, sometimes because peoples needs are different: E.g. someone using it for their own mail server or a corporate mail server where it is possible to yell at the person who turned their mail script into a fork bomb has very different requirements from one that lets "anyone" sign up, for example. That's a good reason for why the extension mechanism is there. As for examples of other things you can do: There are a number of templating languages, for example, that can be demonstrated to always terminate and otherwise be feasible to reason about. I've personally written such template engines also because it was a useful way of preventing the developers from doing stupid things (the ingrates then tried to sneak in a directive to embed a perl interpreter behind my back at one point). You can do a lot more than you might think in such engines by e.g. providing primitives for filtering and iteration over nodes in input graphs (as long as you can't mutate the collections, and there are appropriate termination guarantees e.g. by preventing loops) Another highly useful example that springs to mind is BPF, which while it started as a basic packet filter (e.g. for tcpdump) is increasingly powering much more functionality on Linux for e.g. tracing, and such as for example kernel level enforcement of system call constraints (you can define filters to apply to subsequent code that e.g. outright rejects certain system calls, or applies comparisons to the system call arguments to decide whether to allow or reject them). But I'd say the question you're asking is the wrong one, though. The original point was that when approaching a problem, there is substantial value to be had by asking "how can I subdivide this problem so that as much as possible can be restricted to a less powerful subset?" The Rule of Least Power, basically. Often you will end up with dynamic subsets that are hard to reason about, but as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest. You don't even need to create full blown languages to get this effect - changing the way you write code and effectively create a DSL in the form of API's can often achieve the same effect, but isolating "dangerous" functionality to separate languages often makes it harder to violate the requirements. > It's not important, but that's not what I meant by general reasoning or arbitrary computation. What I meant is that no matter the language you give me (assuming it's useful enough etc.), answering arbitrary questions about arbitrary programs in that language is not feasible That'd be reasonable apart for setting it up for a No True Scotsman with your "assuming it's useful enough etc.". As we've seen with your objections to Sieve, the languages I'm talking about appears to be languages you don't find "useful enough." Since your objections applies to a different set of languages than those I'm talking about, your objections are moot.

pron 9y ago
> as part of the process you can usually confine the parts that are hard to reason about to a smaller portion of the code and reduce the magnitude of the problem, and gain the ability to reason about the rest. Alas, this was proven wrong for verification in 2005. See https://pron.github.io/posts/correctness-and-complexity#correctness-does-not-decompose https://pron.github.io/posts/correctness-and-complexity#corr... > Since your objections applies to a different set of languages than those I'm talking about, your objections are moot. 1. I reject your examples on the ground that they're considered insufficient for their own domains, and in any case are so restricted that you could not compose the lion share of an application from them even without the theorem showing that you cannot reduce the cost of composition by verifying simple components. 2. While I'm happy to further ponder the utility of the languages you listed, you should bear in mind that, say, a Java program using similar constructs to a Sieve program can be reasoned about automatically by current tools, and with relative ease. In other words, a program so simple is easy to reason about whether it's written in a restricted or a non-restricted language, so using those DSLs just increases the cost of verification. However, that does not mean they are not useful. For example, I read that the main design object of Sieve is to allow servers to run untrusted code.