4 ms·

> On the other hand, if you have an actual model of the SQL, then it also doesn't matter whether that model is checked at runtime (dynamic typing) or at compile

> On the other hand, if you have an actual model of the SQL, then it also doesn't matter whether that model is checked at runtime (dynamic typing) or at compile-time (static typing). In either case it will not allow injection attacks, if implemented correctly. It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so. Static types will exhaustively check for you that certain errors aren't possible (vs tests that check a finite number of cases) + compile-time (vs at runtime when the error actually occurs on particular inputs). > And of course the actual place where nastiness happens is the user input, and I haven't yet seen a place that can statically typecheck users. ;-). So, as you point out, you will need to do dynamic checking and sanitising of input. It sounds like you're talking about dynamic (type) checking here when you really mean regular runtime behaviour? You absolutely can at compile-time make sure your program is going to respond in a sensible way to problematic user inputs at runtime e.g. the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime or the user is asked to try again. I wouldn't call the condition that checks if the string is a valid email a dynamic type check. I don't see how user input is different or special from any other value either e.g. it's not like you can predict what exact values are going to come from files, random number generators or from complex calculations during runtime, you just care that they're in the range you expect.

mpweiher 5y ago
> It sounds like you're talking about dynamic (type) checking here when you really mean regular runtime behaviour? No. Quite the opposite. People here confuse "static typing" with "checking stuff", even such obviously dynamic things as "checking outside input". > You absolutely can at compile-time make sure your program is going to respond in a sensible way to problematic user inputs at runtime Right. Sort of. But that is just normal code. Code that absolutely, definitely has to be executed at runtime and at no other time. Because that is when the actual users of your system are going to input the actual data. Not while you're compiling stuff. Your users (and the rest of the world you interact with) aren't there while you're compiling. And your compiler isn't around when your users are inputting data. > the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime No, the compiler cannot verify user input, because the compiler isn't running when the user is inputting data. You can implement a model that has the concept of "valid e-mail", and you can implement your system such that it converts input data such as strings into your structured model at the edges and then only deals with "valid e-mail" objects internally. But implementing such a model has nothing whatsoever to do with whether you use a statically type-checked language or a dynamically type-checked language. It also turns out that such systems tend to be really, really bad. What you actually want to do is keep the user input exactly as it was input, for auditing purposes if nothing else, and build your structures as an enrichment on top of that basic data. Because your idea of what constitutes a "valid" e-mail is almost certainly wrong, and it's better if the system can at least represent data even if it doesn't completely understand it, rather than destroy user data.
- seanwilson 5y ago
  > > the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime or the user is asked to try again. > No, the compiler cannot verify user input, because the compiler isn't running when the user is inputting data. I'm not following why you thought I meant that. It's like you're arguing it's impossible to make any compile-time guarantees because you don't know what exact literal inputs your program will be dealing with at runtime when the field of https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification exists. E.g. at compile time you can prove a sorting function gives the correct output for all possible inputs without having to run the code - you don't know in advance what the input is going to be (which is normal when coding), but you still know the output will be correct with respect to the function specification.
  - mpweiher 5y ago
    No, I am not saying that you cannot make any compile-time guarantees. I am saying that these have little to nothing to do with the actual securing against SQL injection attacks, and that the idea that static types help there is simply an unsupported assumption (and a circular argument, see parallel post).
  - simiones 5y ago
    There are two ways to have the compiler ensure that you produce safe SQL for any user input: 1. Define SQL in your type system, and force programmer to specify for any piece of user input they want to use in a query what its semantics are supposed to be. This is the SQL DSL approach, such as the short lived LINQ-to-SQL or Haskell's Selda. ORMs also do something similar. 2. Enforce that any string sent to the DB passes through some kind of checker that enures certain properties hold for that SQL. The checker will have to understand all of the semantics of SQL, just like in 1. There are many libraries that go through path 1, but don't support the full capabilities of SQL (usually they support a tiny subset), even for a single DB.
mpweiher 5y ago
> It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so This is where the argument became circular and we can basically stop. The parent claim (by chriswarbo) was that, for example, SQL injection attacks were, in fact, incontrovertible proof that SQL injection attacks "are classic type errors". That simply isn't true, at least not in the sense of static type checking (and only made true, as I mentioned above, by conflating "static type", "type" and "model" into one incoherent gooey mush). chriswarbo's incorrect claim was in response to my referenced article, The Safyness of Static Typing [1], where I (as a prelude to my actual point) look at the evidence for the claim that "static types make it easier to implement something correctly". There isn't any. Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. And yes, that article is somewhat old, but the evidentiary situation has not changed, despite further attempts to make the claim that static typing is provably better. Claims that were resoundingly debunked. So that's the background. With this background we have the idea that SQL injection attacks are somehow evidence for the problems with dynamic typing, which they are not. I can have a statically checked string type and have exactly the same SQL injection attacks, and in principle, checking code needs to run at runtime against the dynamic input it is represented with. Which I think we agree on: > It's possible to implement anything correctly with dynamic types but apparently chriswarbo does not. So that brings us to the circularity of the argument: > but the point is static typing makes it easier to do so This hasn't been shown. It was claimed. And it was claimed that SQL injection somehow proves this. Which it doesn't, because we agree that what prevents the attack is the code that runs, the model that executes. It may be that such code is easier to write with static types, but that hasn't been shown, it is just claimed and the claim repeated in support of the claim. Circle. [1] https://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html https://blog.metaobject.com/2014/06/the-safyness-of-static-t...
- seanwilson 5y ago
  > Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. You mean the link from [1] to "An experiment about static and dynamic type systems" based on "an empirical study with 49 [undergraduate] subjects that studies the impact of a static type system for the development of a parser over 27 hours working time.". I think studies like this are more distracting here than useful (low skill level, not large scale enough, too much noise, toy example). The article here sums up a lot of my thoughts on this: https://news.ycombinator.com/item?id=27892615 https://news.ycombinator.com/item?id=27892615 And do you really need a study that proves e.g. (to pick a simpler example to summarise) a language that makes it impossible for null deferences to happen at compile-time is going to have less null dereference errors than one that lets those errors happen at runtime? It's like insisting for an empirical study that 2 + 2 = 4. > It may be that such code is easier to write with static types, but that hasn't been shown, The typed SQL example might look something like: function getUserInput(): string function createSanitisedString(s: string): SanitisedString function createSafeSqlQuery(s: SanitisedString): SqlQuery For the code `createSafeSqlQuery(getUserInput())`, a static type checker would stop the entire program from starting with a type error pinpointing the exact line where the unsanitised data is coming from. With a dynamic type checker: 1. At best, the code will fail only after the user input is received by createSafeSqlQuery during runtime and you won't know where the input originated from. 2. At worst, the coder forgets to add a check like `typeof s === SanitisedString` or a call to `createSanitisedString` in `createSafeSqlQuery` and creates an injection attack. The static type checker clearly wins here for me for safety and ease of implementing correctly. I don't need a study to know that compile-time errors are better than production runtime errors, that automated and exhaustive checks of correctness are better than the coder having to remember to add manual checks, and that it's better to know the exact line the unsanitised input came from over only knowing it comes from somewhere. What languages have you used that have strong static type systems that you've written large programs in? Have you tried OCaml or Haskell for example?

mpweiher 5y ago

> It sounds like you're talking about dynamic (type) checking here when you really mean regular runtime behaviour? No. Quite the opposite. People here confuse "static typing" with "checking stuff", even such obviously dynamic things as "checking outside input". > You absolutely can at compile-time make sure your program is going to respond in a sensible way to problematic user inputs at runtime Right. Sort of. But that is just normal code. Code that absolutely, definitely has to be executed at runtime and at no other time. Because that is when the actual users of your system are going to input the actual data. Not while you're compiling stuff. Your users (and the rest of the world you interact with) aren't there while you're compiling. And your compiler isn't around when your users are inputting data. > the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime No, the compiler cannot verify user input, because the compiler isn't running when the user is inputting data. You can implement a model that has the concept of "valid e-mail", and you can implement your system such that it converts input data such as strings into your structured model at the edges and then only deals with "valid e-mail" objects internally. But implementing such a model has nothing whatsoever to do with whether you use a statically type-checked language or a dynamically type-checked language. It also turns out that such systems tend to be really, really bad. What you actually want to do is keep the user input exactly as it was input, for auditing purposes if nothing else, and build your structures as an enrichment on top of that basic data. Because your idea of what constitutes a "valid" e-mail is almost certainly wrong, and it's better if the system can at least represent data even if it doesn't completely understand it, rather than destroy user data.

seanwilson 5y ago
> > the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime or the user is asked to try again. > No, the compiler cannot verify user input, because the compiler isn't running when the user is inputting data. I'm not following why you thought I meant that. It's like you're arguing it's impossible to make any compile-time guarantees because you don't know what exact literal inputs your program will be dealing with at runtime when the field of https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification exists. E.g. at compile time you can prove a sorting function gives the correct output for all possible inputs without having to run the code - you don't know in advance what the input is going to be (which is normal when coding), but you still know the output will be correct with respect to the function specification.
- mpweiher 5y ago
  No, I am not saying that you cannot make any compile-time guarantees. I am saying that these have little to nothing to do with the actual securing against SQL injection attacks, and that the idea that static types help there is simply an unsupported assumption (and a circular argument, see parallel post).
- simiones 5y ago
  There are two ways to have the compiler ensure that you produce safe SQL for any user input: 1. Define SQL in your type system, and force programmer to specify for any piece of user input they want to use in a query what its semantics are supposed to be. This is the SQL DSL approach, such as the short lived LINQ-to-SQL or Haskell's Selda. ORMs also do something similar. 2. Enforce that any string sent to the DB passes through some kind of checker that enures certain properties hold for that SQL. The checker will have to understand all of the semantics of SQL, just like in 1. There are many libraries that go through path 1, but don't support the full capabilities of SQL (usually they support a tiny subset), even for a single DB.

mpweiher 5y ago

> It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so This is where the argument became circular and we can basically stop. The parent claim (by chriswarbo) was that, for example, SQL injection attacks were, in fact, incontrovertible proof that SQL injection attacks "are classic type errors". That simply isn't true, at least not in the sense of static type checking (and only made true, as I mentioned above, by conflating "static type", "type" and "model" into one incoherent gooey mush). chriswarbo's incorrect claim was in response to my referenced article, The Safyness of Static Typing [1], where I (as a prelude to my actual point) look at the evidence for the claim that "static types make it easier to implement something correctly". There isn't any. Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. And yes, that article is somewhat old, but the evidentiary situation has not changed, despite further attempts to make the claim that static typing is provably better. Claims that were resoundingly debunked. So that's the background. With this background we have the idea that SQL injection attacks are somehow evidence for the problems with dynamic typing, which they are not. I can have a statically checked string type and have exactly the same SQL injection attacks, and in principle, checking code needs to run at runtime against the dynamic input it is represented with. Which I think we agree on: > It's possible to implement anything correctly with dynamic types but apparently chriswarbo does not. So that brings us to the circularity of the argument: > but the point is static typing makes it easier to do so This hasn't been shown. It was claimed. And it was claimed that SQL injection somehow proves this. Which it doesn't, because we agree that what prevents the attack is the code that runs, the model that executes. It may be that such code is easier to write with static types, but that hasn't been shown, it is just claimed and the claim repeated in support of the claim. Circle. [1] https://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html https://blog.metaobject.com/2014/06/the-safyness-of-static-t...

seanwilson 5y ago
> Or to be precise, there isn't any that passes any statistical or other standards. What little evidence there is goes both ways and has, at best, tiny effect sizes. You mean the link from [1] to "An experiment about static and dynamic type systems" based on "an empirical study with 49 [undergraduate] subjects that studies the impact of a static type system for the development of a parser over 27 hours working time.". I think studies like this are more distracting here than useful (low skill level, not large scale enough, too much noise, toy example). The article here sums up a lot of my thoughts on this: https://news.ycombinator.com/item?id=27892615 https://news.ycombinator.com/item?id=27892615 And do you really need a study that proves e.g. (to pick a simpler example to summarise) a language that makes it impossible for null deferences to happen at compile-time is going to have less null dereference errors than one that lets those errors happen at runtime? It's like insisting for an empirical study that 2 + 2 = 4. > It may be that such code is easier to write with static types, but that hasn't been shown, The typed SQL example might look something like: function getUserInput(): string function createSanitisedString(s: string): SanitisedString function createSafeSqlQuery(s: SanitisedString): SqlQuery For the code `createSafeSqlQuery(getUserInput())`, a static type checker would stop the entire program from starting with a type error pinpointing the exact line where the unsanitised data is coming from. With a dynamic type checker: 1. At best, the code will fail only after the user input is received by createSafeSqlQuery during runtime and you won't know where the input originated from. 2. At worst, the coder forgets to add a check like `typeof s === SanitisedString` or a call to `createSanitisedString` in `createSafeSqlQuery` and creates an injection attack. The static type checker clearly wins here for me for safety and ease of implementing correctly. I don't need a study to know that compile-time errors are better than production runtime errors, that automated and exhaustive checks of correctness are better than the coder having to remember to add manual checks, and that it's better to know the exact line the unsanitised input came from over only knowing it comes from somewhere. What languages have you used that have strong static type systems that you've written large programs in? Have you tried OCaml or Haskell for example?