Why we should adopt a non-Turing complete language for client-side scripting(doriantaylor.com)
doriantaylor.com
Why we should adopt a non-Turing complete language for client-side scripting
http://doriantaylor.com/something-i-would-like-to-do
14 comments
>There are plenty of static analysis tools that can determine if programs written in turing-complete languages will halt.
But they're heuristic, which means if their use ever becomes widespread it will be very easy for malicious software writers to defeat them on a case-by-case basis.
But they're heuristic, which means if their use ever becomes widespread it will be very easy for malicious software writers to defeat them on a case-by-case basis.
Yes, this is the operative point. Analyzing intentionally obfuscated code is a whole different deal than analyzing ordinary code. Throw in an interpreter for a bizarre language of your own design, along with some code in that language, and you will frustrate any extant static analyzer.
They need not be heuristic. It is possible to formally prove things about programs in Turing-complete languages.
>It is possible to formally prove things about programs in Turing-complete languages.
But not about arbitrary programs you download from the Internet. For such programs you need to require either that they include a custom proof, or that they're written in a non-Turing complete language so that you can check safety yourself.
But not about arbitrary programs you download from the Internet. For such programs you need to require either that they include a custom proof, or that they're written in a non-Turing complete language so that you can check safety yourself.
... or you could adopt a personal policy of just not running such programs. That's the top-level poster's point -- the boundary between statically-analyzable and not is extremely complex, and not coincident with Turing-completeness.
Turing-completeness is difficult to avoid, and has little to do with security. For every addition to the language—browser extensions in particular—we will have to very carefully prove that it cannot introduce any way to create a non-terminating function.
But in any non-trivial interactive application, termination can’t be a guarantee. The user may not ever cause the program to halt, and indeed, you want a game to run without end. Perhaps you could use a form of FRP: only the reactive part of a program would run continuously. But what would you gain?
We don’t need to make a language where programs are provably innocent. We need to make a language where assumed-guilty programs are provably imprisonable! An ordinary statically typed functional language would do just fine.
But in any non-trivial interactive application, termination can’t be a guarantee. The user may not ever cause the program to halt, and indeed, you want a game to run without end. Perhaps you could use a form of FRP: only the reactive part of a program would run continuously. But what would you gain?
We don’t need to make a language where programs are provably innocent. We need to make a language where assumed-guilty programs are provably imprisonable! An ordinary statically typed functional language would do just fine.
>Turing-completeness is difficult to avoid [...] For every addition to the language [...] we will have to very carefully prove that it cannot introduce any way to create a non-terminating function.
Solving the halting problem doesn't mean all programs end - it means you can automatically determine whether an arbitrary program ends.
Solving the halting problem doesn't mean all programs end - it means you can automatically determine whether an arbitrary program ends.
Yes. So? We’re not talking about the halting problem. The author wrote of total functional programming, a paradigm in which all functions and programs are provably terminating.
> we will have to very carefully prove that it cannot introduce any way to create a non-terminating function
>The author wrote of total functional programming, a paradigm in which all functions and programs are provably terminating.
So then what are you concerned about? Either use TFP, if indeed all your programs terminate, or have a different non-Turing complete approach, in which case you can still write infinite loops.
>The author wrote of total functional programming, a paradigm in which all functions and programs are provably terminating.
So then what are you concerned about? Either use TFP, if indeed all your programs terminate, or have a different non-Turing complete approach, in which case you can still write infinite loops.
I think this is not a good idea.
1. what kind of security properties do you want to verify. I cannot think of one that could not be checked at runtime when the dangerous function is called with actual parameters.
2. turing completeness has nothing to do with security. Before Haskell had IO it was totally safe but still turing complete.
1. what kind of security properties do you want to verify. I cannot think of one that could not be checked at runtime when the dangerous function is called with actual parameters.
2. turing completeness has nothing to do with security. Before Haskell had IO it was totally safe but still turing complete.
While the sentiment is understandable, this solution is technical drivel. The concern is security, and could be solved by further restricting permissions in the browser. Anyone familiar with computabiliy would know that changing the language will not help. You could improve the situation today with a restrictive browser plugin.
[deleted](1)
This raises an interesting question that I hadn't considered before: how many of the programs that we write every day actually rely on the Turing-completeness of their underlying languages? If the statically-verifiable properties of, whaddya call it, strong functional programming outweigh the loss of expressiveness, there could be a big market for general-purpose (is that a contradiction?) languages of this bent.
Throw it on the pile of Things That Could Be The Next Big Thing, Maybe--right on top of declarative programming and highly-concurrent programming.
Throw it on the pile of Things That Could Be The Next Big Thing, Maybe--right on top of declarative programming and highly-concurrent programming.
I agree with what appears to be your general goal, but various points:
1. You need to refine your argument. I suspect your main point is philosophical and political, but you detract from it by setting up a nebulous security argument. The security concerns you describe are non-issues. Turing completeness says nothing of the available IO primitives, hence why people counter with sandboxing. Solving XSS is as conceptually simple as having any js-initiated request include the identity of what initiated it (in the case of XSS, the other site), and server frameworks having a whitelist of such initiators. But in general, a user shouldn't be even worried about cross site scripting as they're not meant to have control over it - their only input is whether to rely on the total security of a specific site.
2. Executable blobs are the lowest common denominator (any concept can be realized in them) so new concepts tend to be implemented in them rather than engineering a more declarative format. Furthermore, users are lazy and auto-updating of software (in this case, on every page load) is a net win. However, apt-get also gives me these very nice properties.
3. This is where the philosophy comes in - users should be in control of the software they use! Web 2.0 is actually proprietary software 2.0! Browser extensions can modify the applications to some extent, but are fighting an uphill battle due to the difficulty in analyzing Turing-complete blobs. I presume this is your real motivating factor in wanting to change the expressive power of scripts, but as long as the code has more expressiveness than a simple declarative format, you can never actually tame it. (Imagine a server framework that re-obfuscates the client-side code every hour).
4. One fundamental issue to address is naming the code so that end users may gain control over administering it. One doesn't install a new version of CAD software in the middle of a project, as their goal is to finish the project and not get bogged down figuring out how to use a new version. I only dist-upgrade when I'm willing to accept a few days of shaking out changes. Contrast with the current web, where a site will make unilateral changes and the only recourse of users is to complain. One should be able to locally 'roll back to the previous version of this site', and the site should support that by decoupling their code and data model.
5. Another major issue is data store and "network" independence. If one doesn't like the changes site A is making to the software, they should be able to switch to a competing site B, and have their data and connections intact - akin to several programs using the same file format. This of course requires fundamental site openness, with is directly counter to the standard web-hollywood business model of becoming the middleman in an n^2 network, so I expect eventual disruption rather than gradual change.
1. You need to refine your argument. I suspect your main point is philosophical and political, but you detract from it by setting up a nebulous security argument. The security concerns you describe are non-issues. Turing completeness says nothing of the available IO primitives, hence why people counter with sandboxing. Solving XSS is as conceptually simple as having any js-initiated request include the identity of what initiated it (in the case of XSS, the other site), and server frameworks having a whitelist of such initiators. But in general, a user shouldn't be even worried about cross site scripting as they're not meant to have control over it - their only input is whether to rely on the total security of a specific site.
2. Executable blobs are the lowest common denominator (any concept can be realized in them) so new concepts tend to be implemented in them rather than engineering a more declarative format. Furthermore, users are lazy and auto-updating of software (in this case, on every page load) is a net win. However, apt-get also gives me these very nice properties.
3. This is where the philosophy comes in - users should be in control of the software they use! Web 2.0 is actually proprietary software 2.0! Browser extensions can modify the applications to some extent, but are fighting an uphill battle due to the difficulty in analyzing Turing-complete blobs. I presume this is your real motivating factor in wanting to change the expressive power of scripts, but as long as the code has more expressiveness than a simple declarative format, you can never actually tame it. (Imagine a server framework that re-obfuscates the client-side code every hour).
4. One fundamental issue to address is naming the code so that end users may gain control over administering it. One doesn't install a new version of CAD software in the middle of a project, as their goal is to finish the project and not get bogged down figuring out how to use a new version. I only dist-upgrade when I'm willing to accept a few days of shaking out changes. Contrast with the current web, where a site will make unilateral changes and the only recourse of users is to complain. One should be able to locally 'roll back to the previous version of this site', and the site should support that by decoupling their code and data model.
5. Another major issue is data store and "network" independence. If one doesn't like the changes site A is making to the software, they should be able to switch to a competing site B, and have their data and connections intact - akin to several programs using the same file format. This of course requires fundamental site openness, with is directly counter to the standard web-hollywood business model of becoming the middleman in an n^2 network, so I expect eventual disruption rather than gradual change.
It's possible to make JavaScript not be Turing-complete. You could place a limit on the number of instructions the program could execute, or a limit on the amount of memory (including network transfers), either of which would make it mathematically possible to determine whether or not the program halts.
However, this doesn't mean it's feasible, and if the language is useful it's probably not. You can pick an NP-complete problem with a large input data set and make halting depend upon the outcome. It will take a very long time to determine if such an application halts or not, since you have to solve the NP-complete problem.
Of course, if you care only about states the application could potentially reach, instead of those it actually does reach, you could do this much faster. However, if you know which states are undesirable, you can check if you are reaching them during runtime as well.
However, this doesn't mean it's feasible, and if the language is useful it's probably not. You can pick an NP-complete problem with a large input data set and make halting depend upon the outcome. It will take a very long time to determine if such an application halts or not, since you have to solve the NP-complete problem.
Of course, if you care only about states the application could potentially reach, instead of those it actually does reach, you could do this much faster. However, if you know which states are undesirable, you can check if you are reaching them during runtime as well.
This is a much less revolutionary proposal than it may seem. The web already features extensive use of a non-Turing complete language. It's a less-appreciated feature of SQL, but it makes defense against nasty attacks at least feasible (if not always applied).
Another important advantage is query optimization. Programs in non-Turing complete languages can be automatically analyzed, not only to determine their security implications, but also to rewrite them in optimal form. In a good NTCL with an optimizer, you don't care how (in)efficient your algorithms are - they're automatically upgraded to their theoretical fastest speed.
Another important advantage is query optimization. Programs in non-Turing complete languages can be automatically analyzed, not only to determine their security implications, but also to rewrite them in optimal form. In a good NTCL with an optimizer, you don't care how (in)efficient your algorithms are - they're automatically upgraded to their theoretical fastest speed.
The standard may not be Turing complete, but I know of no decent SQL implementation that isn't; they've all added loops or some form of cursor.
Never claimed it was revolutionary. ;)
The parent's point is that there is a (slightly) lower barrier to adoption due to the not-as-revolutionary-as-it-seems nature of the idea (i.e. it is arguing in favour of the idea).
Ah, sorry. Trying to get out the door here. heh
It seems there's some doubt in the comments that Turing completeness is relevant to security. Here's a simple proof it is. Assume you have an arbitrary function to execute and a set of no-nos (forbidden operations, machine states etc.). If you know for sure the function does nothing forbidden before its executions ends, you also know for sure that its execution ends. So you've solved the halting problem - which means your original function couldn't have been written in a Turing complete language, for which the halting problem is unsolvable.
If you want to prove that a complicated function which contains a forbidden line will ever actually execute that line given any input, then yes, the turing-completeness of Javascript makes it difficult to prove that the function is safe, because you can't even prove that it will ever halt, let alone reach a line. But imagine that Javascript were simpler--say, it could only contain the control flow constructs if, !, &&, ||. Then, in order to prove that a complicated function never reaches a forbidden line, you have to solve a 3-SAT problem, which is NP-complete and also impractical to prove for all functions.
The only sure way to prove that a function is safe, turing-complete or not, is to restrict the system calls it can make.
I agree that if you provide domain-specific non-turing complete languages, it's more likely that you will be able to grok it and pull it apart, but it doesn't let you prove that any arbitrary function doesn't reach a line you don't like for all user input.
The only sure way to prove that a function is safe, turing-complete or not, is to restrict the system calls it can make.
I agree that if you provide domain-specific non-turing complete languages, it's more likely that you will be able to grok it and pull it apart, but it doesn't let you prove that any arbitrary function doesn't reach a line you don't like for all user input.
Your total functional programming does not solve the problem at hand. TFP prevents you from creating a program that never halts, but it does nothing to prevent you from creating an incomprehensible program that takes 1e10000 years to compute.
I don't know anything about TFP personally or whether it's the best tool for this job. (I just agree with the job description.) And you misunderstand the halting problem - you can perfectly well write never-ending programs in a non-Turing complete language. The only difference is that you can tell whether an arbitrary program ends or not.
I don't know anything about TFP personally or whether it's the best tool for this job
To say that you don't know anything about it while claiming it will solve our problems is ... dishonest at best.
And you misunderstand the halting problem - you can perfectly well write never-ending programs in a non-Turing complete language. The only difference is that you can tell whether an arbitrary program ends or not.
I don't think that you understand the implications of the halting problem. You are claiming that use of a Turing incomplete language will make automated verification of programs possible, and that this automated verification will save us from web pages doing things that we do not want. I will suggest that any solid academic would not think highly of your argument.
Here's a simple experiment that might help you understand an important flaw in your argument. Determining the range of a short program takes a small amount of time, a longer program takes longer. TPS is a restricted language which allows for programs of any length, as long as they will eventually halt. If I write a huge, complex program, and it will take forever minus a day to halt, how long do you think it will take to verify? Spoiler Alert! Longer than you will wait for a web page to load.
The way that we use computers as society is not very academic. If you want to build a web browser that doesn't browse the web, you will find yourself quite lonely.
To say that you don't know anything about it while claiming it will solve our problems is ... dishonest at best.
And you misunderstand the halting problem - you can perfectly well write never-ending programs in a non-Turing complete language. The only difference is that you can tell whether an arbitrary program ends or not.
I don't think that you understand the implications of the halting problem. You are claiming that use of a Turing incomplete language will make automated verification of programs possible, and that this automated verification will save us from web pages doing things that we do not want. I will suggest that any solid academic would not think highly of your argument.
Here's a simple experiment that might help you understand an important flaw in your argument. Determining the range of a short program takes a small amount of time, a longer program takes longer. TPS is a restricted language which allows for programs of any length, as long as they will eventually halt. If I write a huge, complex program, and it will take forever minus a day to halt, how long do you think it will take to verify? Spoiler Alert! Longer than you will wait for a web page to load.
The way that we use computers as society is not very academic. If you want to build a web browser that doesn't browse the web, you will find yourself quite lonely.
To reply to posts without bothering to understand them is... not worth responding to. I have a PhD in CS from an Ivy League school BTW, so spare me the "solid academic" lecturing.
To reply to posts without bothering to understand them is... not worth responding to.
I think that I've done a passable job at understanding the argument and providing sound counter arguments. To each their own opinion.
I have a PhD in CS from an Ivy League school BTW, so spare me the "solid academic" lecturing.
One remark is hardly a lecture, but great to appeal to credentialism. That's the Ivy League spirit! I on the other hand have a mere bachelors degree; from a public school no less! I would jokingly admit defeat, but my school taught me that defeat is for the defeated.
I won't ask which Ivy League school - their reputation in computer science is low enough already.
I think that I've done a passable job at understanding the argument and providing sound counter arguments. To each their own opinion.
I have a PhD in CS from an Ivy League school BTW, so spare me the "solid academic" lecturing.
One remark is hardly a lecture, but great to appeal to credentialism. That's the Ivy League spirit! I on the other hand have a mere bachelors degree; from a public school no less! I would jokingly admit defeat, but my school taught me that defeat is for the defeated.
I won't ask which Ivy League school - their reputation in computer science is low enough already.
The halting problem doesn't mean that you can't prove that some programs halt. It just means that you can't prove whether every program halts (or doesn't). If I write a program:
int main () { return 0; }
I can easily prove that it will halt. There are some classes of programs that provably halt, and some classes that provably don't. Proving that a program halts doesn't mean anything about solving the halting problem, and it doesn't say anything about the Turing-completeness of the language.
int main () { return 0; }
I can easily prove that it will halt. There are some classes of programs that provably halt, and some classes that provably don't. Proving that a program halts doesn't mean anything about solving the halting problem, and it doesn't say anything about the Turing-completeness of the language.
Right, so an alternative approach is to require all client-side scripts that your browser downloads to come with a proof of safety. This requires extra work for each script. Which can be avoided if the script language was non-Turing complete instead, and you had a general-purpose code analyzer on your machine.
It depends on what you forbid. If you want to be able to forbid arbitrary program states without running the program, then yeah, you’re out of luck. But if you just want to forbid, say, cross-site requests, then that’s perfectly doable through ordinary sandboxing. Sure, it’s done at runtime, but does that much matter?
The nay-sayers might be right, but I think this is an interesting suggestion. If data flow analysis is easier in a TFP language, it would certainly make my life easier (I work in the security static analysis business). It seems like it might be easier, since higher-order control flow is definitely a problem for data flow analysis, and TFP languages can't have higher-order control flow because that would open the door to arbitrary recursion.
So I'm not sure what I think about this yet, except that it's interesting to chew on.
So I'm not sure what I think about this yet, except that it's interesting to chew on.
FYI I've already gotten some feedback re the (human attention and computational) cost of proof systems. I'm not sure yet if this problem is (exactly) the same as that.
And this in a day where CSS is turing-complete...
make sure to check out http://elm-lang.org
it's not what you are searching for but it might be fairly easy to turn it into what you describe.
the creator of elm-lang, Evan Czaplicki, told me he'll opensource it rather soon. of all functional-JS buzz out there, this one makes most sense to me.
it's not what you are searching for but it might be fairly easy to turn it into what you describe.
the creator of elm-lang, Evan Czaplicki, told me he'll opensource it rather soon. of all functional-JS buzz out there, this one makes most sense to me.
Interesting idea. It fits in well with a capability model of security. Also note, that as more computing happens on the web, the JavaScript sandbox becomes less meaningful.
This is categorically false. There are plenty of static analysis tools that can determine if programs written in turing-complete languages will halt. They can't do it for every program, but they can do it for large numbers of useful programs.
Simple counterexample: python is turing complete, yet it is possible to mechanically analyze and determine a whole lot about this program:
Yes, that's a stupid example, but it demonstrates that the premise of this article is false.
As further example that the author misunderstands the issue is the quote: "That, or viewing your website means I have to pore over every line." If good static analysis tools can't figure it out, it is less likely that a person will.
Static analysis tools running on Turing complete languages are a useful tool. Sometimes they answer "I don't know" at which point you will have to decide if you trust the author or not, but the vast majority of code out there is fairly tractable.
[edit] It is true that it is a mathematical impossibility for all possible programs in a turing-complete language to be analyzed, but that doesn't mean that there don't exist programs that are analyzable and has little bearing on whether or not real-world programs are analyzable.