6 ms·

The problem is that often getting rid of these type-unsafe idioms requires much more sophisticated types OR much more tedious code than expected. For example, a

The problem is that often getting rid of these type-unsafe idioms requires much more sophisticated types OR much more tedious code than expected. For example, a language without NULL references must rely on something like Optional/Maybe. Optional requires generic types (kind-1 types) to be usable, and it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. The SQL case is much more complex. SQL is such a non-standardized language in practice, and such a complex one, that trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex. So, you end up with convenient string->SQL converters, and then people stick untrusted input in those strings. Not to mention, your fancy AST library still needs to spit out SQL text to talk to most DBs, so you end up needing to sanitize identifiers in your own SQL->string conversion.

mpweiher 5y ago
Right. The other thing is that in the parent, "static type checking" got shortened to "types", which in turn got confused with "modelling". The problem with stringly-typing is the model, which is SQL as strings. Statically type-checking that all your strings are, in fact, strings does not buy you anything whatsoever in this scenario. 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. 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.
- chriswarbo 5y ago
  > 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. ;-) User input has type `ByteString`. Not only can we check that statically, we absolutely should; and we should enforce that type, to reject any code which assumes otherwise. Nastiness happens when developers treat user input as something other than ByteString; e.g. they might try appending it to a fragment of HTML (XSS); or wrap it in quotation marks and send it to a database (SQL injection). We don't need to 'statically typecheck users'; we do need to statically check that `myApp` has type `ByteString -> Foo`, so we can avoid ever executing implementations which actually have type `HTMLFragment -> Foo` (XSS), or `SQLFragment -> Foo` (SQL injection), or whatever.
- deleted 5y ago
  [deleted]
- seanwilson 5y ago
  > 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.
chriswarbo 5y ago
> Optional requires generic types (kind-1 types) to be usable My gut tells me that's not quite right (for some reasonable definition of 'usable'), since we can always build elimination forms into the language (after all, 'null' must be built in, and few take objection to building in elimination forms like if/then/else). > it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. I really like comprehensions in Python, but hardly ever use them elsewhere. In fact, when I do use them in Haskell and Scala, I usually find myself having to refactor them into calls to `map`/`join`/etc. soon after, to have more fine-grained scoping or somesuch. > trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex That's orthogonal to anything I said. Represent SQL using arrays of bytes in memory if you like; offer a string-like interface for constructing and manipulating them if you like; just make sure to distinguish them from other string-like types, in a way that's statically enforceable, and where the only API to convert a 'String' to an 'SQL' is the escaping function. Note that I don't particularly care if an SQL value is valid; it would be nice to statically enforce that, but you're right that (vendor-supplied) SQL is pretty complex in its own right. What's much more important to get right is that SQL is not user-generated.
- simiones 5y ago
  > My gut tells me that's not quite right (for some reasonable definition of 'usable'), since we can always build elimination forms into the language (after all, 'null' must be built in, and few take objection to building in elimination forms like if/then/else). True, you could go the Go array route and have Optional be a special type that is generic, without otherwise supporting generic data structures. > I really like comprehensions in Python, but hardly ever use them elsewhere. I think code like possiblyMissing.map(value => code) introduces lots of unpleasant imbrication, and breaking out functions for every possibly-missing value also seems to me to lead to bad readability. I suppose this may be a matter of taste, or it may be related to other language features. > just make sure to distinguish them from other string-like types, in a way that's statically enforceable, and where the only API to convert a 'String' to an 'SQL' is the escaping function. I think this is the part that doesn't really work, because, in order to escape a piece of user input, you need to understand what it's meant to be. For example, a common (unsafe) idiom is: sqlFormatString = "SELECT %s FROM %s WHERE %s;"; filterFormatString = "%s LIKE ?"; filterString = sprintf(filterFormatString, userInputColumnName); sqlQuery = sprintf(sqlFormatString, columnName, tableName, filterString); preparedQuery = dbImpl.prepare(sqlQuery, userInputValue); Which of course does the right thing for userInputValue; may or may not be doing the right thing with columnName and tableName, depending on the source; and does the really wrong thing with userInputColumn. Now, you could replace this with a type safe dbImpl.prepare(), which only takes a NotUserGeneratedSQL type. But now you need to have some way to build a NotUserGeneratedSQL. One option is to go all in on an SQL AST library, where you could build the query above like query = selectQuery(); query.columnNames = [ escapeColName(columnName) ]; query.from = escapeTableName(tableName); queryFilter = equalityComparison(); queryFilter.left = escapeColName(userInputColumn); queryFilter.right = preparedArg(); query.filter = queryFilter; preparedQuery = dbImpl.prepare(query, userInputValue) But this, as I said, gets tedious for the user and complex for the implementer. However, I don't think there is any alternative that can actually enforce validation of user input in constructed queries. You can help users think about it by forcing them to use some kind of string -> NotUserGeneratedSQL function, but this function can't actually be written to reject the example I gave initially. A function that creates an empty minimal NotUserGeneratedSQL and offers other functions to build it up to a useful query will either accept strings (making it possible to introduce SQL injection) or have to accept structured SQL, making it fall into the AST problem. Of course, the problem of NotUserGeneratedSQL is easy if you don't want to support any kind of dynamic query, other than prepared statements. But if you want to dynamically generate queries based on user input (e.g. user chooses which columns they want to see, which columns they want to filter by etc.), then I don't think it's possible to statically ensure that SQL injection is not possible without an ORM or SQL AST API. Edit: if you believe otherwise, please show me a type-safe, SQL-injection-safe library in any language that isn't an ORM/EDSL or a straight up SQL AST manipulator. I am quite certain none exists, but I would be happy to be proven wrong.

mpweiher 5y ago

Right. The other thing is that in the parent, "static type checking" got shortened to "types", which in turn got confused with "modelling". The problem with stringly-typing is the model, which is SQL as strings. Statically type-checking that all your strings are, in fact, strings does not buy you anything whatsoever in this scenario. 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. 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.

chriswarbo 5y ago
> 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. ;-) User input has type `ByteString`. Not only can we check that statically, we absolutely should; and we should enforce that type, to reject any code which assumes otherwise. Nastiness happens when developers treat user input as something other than ByteString; e.g. they might try appending it to a fragment of HTML (XSS); or wrap it in quotation marks and send it to a database (SQL injection). We don't need to 'statically typecheck users'; we do need to statically check that `myApp` has type `ByteString -> Foo`, so we can avoid ever executing implementations which actually have type `HTMLFragment -> Foo` (XSS), or `SQLFragment -> Foo` (SQL injection), or whatever.
deleted 5y ago
[deleted]
seanwilson 5y ago
> 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.

chriswarbo 5y ago

> Optional requires generic types (kind-1 types) to be usable My gut tells me that's not quite right (for some reasonable definition of 'usable'), since we can always build elimination forms into the language (after all, 'null' must be built in, and few take objection to building in elimination forms like if/then/else). > it also requires some kind of pattern matching or monad comprehensions - otherwise, code using Optional is neither type safe nor readable. I really like comprehensions in Python, but hardly ever use them elsewhere. In fact, when I do use them in Haskell and Scala, I usually find myself having to refactor them into calls to `map`/`join`/etc. soon after, to have more fine-grained scoping or somesuch. > trying to offer a generic SQL library that presents an AST as the API for even the most popular RDBMSs quickly gets complex That's orthogonal to anything I said. Represent SQL using arrays of bytes in memory if you like; offer a string-like interface for constructing and manipulating them if you like; just make sure to distinguish them from other string-like types, in a way that's statically enforceable, and where the only API to convert a 'String' to an 'SQL' is the escaping function. Note that I don't particularly care if an SQL value is valid; it would be nice to statically enforce that, but you're right that (vendor-supplied) SQL is pretty complex in its own right. What's much more important to get right is that SQL is not user-generated.

simiones 5y ago
> My gut tells me that's not quite right (for some reasonable definition of 'usable'), since we can always build elimination forms into the language (after all, 'null' must be built in, and few take objection to building in elimination forms like if/then/else). True, you could go the Go array route and have Optional be a special type that is generic, without otherwise supporting generic data structures. > I really like comprehensions in Python, but hardly ever use them elsewhere. I think code like possiblyMissing.map(value => code) introduces lots of unpleasant imbrication, and breaking out functions for every possibly-missing value also seems to me to lead to bad readability. I suppose this may be a matter of taste, or it may be related to other language features. > just make sure to distinguish them from other string-like types, in a way that's statically enforceable, and where the only API to convert a 'String' to an 'SQL' is the escaping function. I think this is the part that doesn't really work, because, in order to escape a piece of user input, you need to understand what it's meant to be. For example, a common (unsafe) idiom is: sqlFormatString = "SELECT %s FROM %s WHERE %s;"; filterFormatString = "%s LIKE ?"; filterString = sprintf(filterFormatString, userInputColumnName); sqlQuery = sprintf(sqlFormatString, columnName, tableName, filterString); preparedQuery = dbImpl.prepare(sqlQuery, userInputValue); Which of course does the right thing for userInputValue; may or may not be doing the right thing with columnName and tableName, depending on the source; and does the really wrong thing with userInputColumn. Now, you could replace this with a type safe dbImpl.prepare(), which only takes a NotUserGeneratedSQL type. But now you need to have some way to build a NotUserGeneratedSQL. One option is to go all in on an SQL AST library, where you could build the query above like query = selectQuery(); query.columnNames = [ escapeColName(columnName) ]; query.from = escapeTableName(tableName); queryFilter = equalityComparison(); queryFilter.left = escapeColName(userInputColumn); queryFilter.right = preparedArg(); query.filter = queryFilter; preparedQuery = dbImpl.prepare(query, userInputValue) But this, as I said, gets tedious for the user and complex for the implementer. However, I don't think there is any alternative that can actually enforce validation of user input in constructed queries. You can help users think about it by forcing them to use some kind of string -> NotUserGeneratedSQL function, but this function can't actually be written to reject the example I gave initially. A function that creates an empty minimal NotUserGeneratedSQL and offers other functions to build it up to a useful query will either accept strings (making it possible to introduce SQL injection) or have to accept structured SQL, making it fall into the AST problem. Of course, the problem of NotUserGeneratedSQL is easy if you don't want to support any kind of dynamic query, other than prepared statements. But if you want to dynamically generate queries based on user input (e.g. user chooses which columns they want to see, which columns they want to filter by etc.), then I don't think it's possible to statically ensure that SQL injection is not possible without an ORM or SQL AST API. Edit: if you believe otherwise, please show me a type-safe, SQL-injection-safe library in any language that isn't an ORM/EDSL or a straight up SQL AST manipulator. I am quite certain none exists, but I would be happy to be proven wrong.