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.
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 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.
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).
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.
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.
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.
[The parent was deleted, but doesn't matter.]
The post is riddled with technical inaccuracies.
because JavaScript is Turing-complete, which any antivirus researcher can tell you is why they still have a job
Viruses exploit security vulnerabilities to self replicate and assume control. They can be written in non Turning complete languages.
the facet of JavaScript's behaviour I'm interested in preventing is in the family of cross-site scripting and request forgeries
Gimping JS would have no effect on this. Increasing browser security would. We have XSS/XSRF because we explicitly allow some cross site communication. Reduce or disallow it and your problem is solved.
The way to get what I want would be to look into the code before running it and selectively disable certain behaviour.
You don't need to fully understand a piece of code to restrict it's actions. This is what a sandbox is.
I hear tell that there's even a company that brokers distributed computing tasks, taking money on one end from customers and paying website owners on the other end to pass on to their users to execute for free.
There is nothing you can do about this, short of personally inspecting the source code. Which in this case will certainly be obfuscated to prevent you from easily understanding it.
His response was probably, but I'd still have the problem of proving code correctness—a perfectly legitimate concern.
The person who defined the idea that the author defers to told him that it wouldn't solve the problem. Why are we still talking?
But the point is, this is totally doable. The theory is sound,
Where was this shown?
there's high-profile demand for it
Where was this shown? I personally would not use a web browser that wasn't compatible with the web.
To top it off, the email link provides the brogrammer subject "yo dawg i herd u like TFP"
I don't see how anyone has upvoted this article. If you care about browser security, you might be interested in building better sandboxes based on Capabilities[1]. What the poster has shown is a misunderstanding for both the technical problem as well as the reality of why we run JavaScript in the browser: because web pages are written in JavaScript. All attempts to do anything about that have failed the market.
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.
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.
>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.
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.
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.
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 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.
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 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.
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.
The amount of effort that would be needed to shift from a Turing complete language to a non Turing complete would outweigh the benefits by a very large amount.
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.
"It is a mathematical impossibility for the behaviour of Turing-complete code to be analyzed by machine."
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:
print "Hello, World!"
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.
>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.
>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.
... 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.
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.
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.
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.
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.
42 comments
[ 3.2 ms ] story [ 80.5 ms ] threadAnother 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.
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.
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.
because JavaScript is Turing-complete, which any antivirus researcher can tell you is why they still have a job
Viruses exploit security vulnerabilities to self replicate and assume control. They can be written in non Turning complete languages.
the facet of JavaScript's behaviour I'm interested in preventing is in the family of cross-site scripting and request forgeries
Gimping JS would have no effect on this. Increasing browser security would. We have XSS/XSRF because we explicitly allow some cross site communication. Reduce or disallow it and your problem is solved.
The way to get what I want would be to look into the code before running it and selectively disable certain behaviour.
You don't need to fully understand a piece of code to restrict it's actions. This is what a sandbox is.
I hear tell that there's even a company that brokers distributed computing tasks, taking money on one end from customers and paying website owners on the other end to pass on to their users to execute for free.
There is nothing you can do about this, short of personally inspecting the source code. Which in this case will certainly be obfuscated to prevent you from easily understanding it.
His response was probably, but I'd still have the problem of proving code correctness—a perfectly legitimate concern.
The person who defined the idea that the author defers to told him that it wouldn't solve the problem. Why are we still talking?
But the point is, this is totally doable. The theory is sound,
Where was this shown?
there's high-profile demand for it
Where was this shown? I personally would not use a web browser that wasn't compatible with the web.
To top it off, the email link provides the brogrammer subject "yo dawg i herd u like TFP"
I don't see how anyone has upvoted this article. If you care about browser security, you might be interested in building better sandboxes based on Capabilities[1]. What the poster has shown is a misunderstanding for both the technical problem as well as the reality of why we run JavaScript in the browser: because web pages are written in JavaScript. All attempts to do anything about that have failed the market.
[1 | http://en.wikipedia.org/wiki/Capability-based_security]
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.
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.
Solving the halting problem doesn't mean all programs end - it means you can automatically determine whether an arbitrary program ends.
>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.
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.
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.
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.
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.
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.
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 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.
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.
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.
So I'm not sure what I think about this yet, except that it's interesting to chew on.