4 ms·

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

by zeteo 15y ago

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.

ynniv 15y ago
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.
- aidenn0 15y ago
  Not to mention the fact that much software (at the source level at least) never terminates by design.
  - zeteo 15y ago
    Yes, some software needs to run in an infinite loop. You can still prove that a single iteration of the loop is safe.
- zeteo 15y ago
  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.
  - ynniv 15y ago
    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.
    - zeteo 15y ago
      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.
      - ynniv 15y ago
        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.
evincarofautumn 15y ago
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?
sp332 15y ago
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.
- zeteo 15y ago
  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.
  - deleted 15y ago
    [deleted]
  - sp332 15y ago
    Oh, I see. Turing-complete language + certificate of good behavior = non-turing-complete language. Cool :)
  - nwmcsween 15y ago
    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.
yonran 15y ago
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.

by zeteo 15y ago

ynniv 15y ago

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.

aidenn0 15y ago
Not to mention the fact that much software (at the source level at least) never terminates by design.
- zeteo 15y ago
  Yes, some software needs to run in an infinite loop. You can still prove that a single iteration of the loop is safe.
zeteo 15y ago
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.
- ynniv 15y ago
  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.
  - zeteo 15y ago
    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.
    - ynniv 15y ago
      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.

evincarofautumn 15y ago

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?

sp332 15y ago

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.

zeteo 15y ago
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.
- deleted 15y ago
  [deleted]
- sp332 15y ago
  Oh, I see. Turing-complete language + certificate of good behavior = non-turing-complete language. Cool :)
- nwmcsween 15y ago
  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.

yonran 15y ago

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.