7 ms·

I have the feeling that Haskell has one feature that could be super useful for security. That feature is the explicit typing of effects via monads. Just look a

I have the feeling that Haskell has one feature that could be super useful for security. That feature is the explicit typing of effects via monads. Just look at the recent log4j example: If effects were explicitly typed in Java, you would potentially scratch your head why you need a network monad or a "insert code into the process" effect to just log a line. Of course, in current Haskell, everything is put into the same IO monad. But in principle, I think that effect systems could have a very nice effect on software security.

lelanthran 5y ago
> I have the feeling that Haskell has one feature that could be super useful for security. > > That feature is the explicit typing of effects via monads. Just look at the recent log4j example: If effects were explicitly typed in Java, you would potentially scratch your head why you need a network monad or a "insert code into the process" effect to just log a line. That would not have helped - the network access with RCE was a feature put into the library. What does the language selection have to do with a feature request of "We want evaluated log strings to be able to do network access with RCE"? There's nothing special in any language (even Haskell) that will prevent this sort of thing.
- Buttons840 5y ago
  > What does the language selection have to do with a feature request of Only functions with certain type signatures can do IO in Haskell. This could be broken down to be more granular such that the type system makes it clear (and even somewhat of a burden) to the caller whether writing to disk happens, or network access, or both. Imagine the entry point to your program is given all "Effects", and then must pass them down the call stack as needed to other functions. Without the appropriate Effect, a function cannot perform the Effect. People might wonder why they were required to pass the NetworkAccess Effect into their logging calls.
  - stonemetal12 5y ago
    Let's just hope there is a "load and execute random code from the network" effect that you could disable. NetworkAccess Effect wouldn't be that strange for a logging system that supports multiple networked log managers like syslog.
    - Quekid5 5y ago
      The point isn't so much that you can disable effects. It's that you literally have no effects/capabilities unless specifically granted. That said, I'm a bit skeptical that Haskell would have prevented this particular issue in practice. The logging monad would just likely just have been called a LoggingM (in MTL style) and most users would have been oblivious as to exactly what it was doing... and as you say: Logging to a remote system needs the network. I guess what could have saved a Haskell program here is that there's no such thing as "download code and execute it with the same privileges as you" with being very explicit about that. (E.g. calling 'system' or whatever)
      - Akronymus 5y ago
        You could split it up into 2 functions I guess. A pure one that creates the log entry, then an IO one that actually saves it.
        Quekid5 5y ago
        Yes, but if the IO one does <shenanigans> then you're as well off. Which is... not very. EDIT: Just to say: I don't mean to be flippant.
        Akronymus 5y ago
        Oh its fine. And i meanr it more in that one part is literally just passing the data along, while the other part generates the data with being fed whatever is needed for it to. so, if yoj want to just log a literal string yoj wouldnt provide any additional functionality to the generator. if you want it to expand strings, then you provide a function for that. and so on
- griffinmb 5y ago
  The point is that with a powerful Effects system, devs calling the logger would have to account for the network call in their own code. Someone might have wondered why that was needed and gotten this addressed before it was ever widespread.
  - lelanthran 5y ago
    > The point is that with a powerful Effects system, devs calling the logger would have to account for the network call in their own code. Someone might have wondered why that was needed and gotten this addressed before it was ever widespread. No one would have wondered anything - it's a networked logger, with network functionality.
  - inkeddeveloper 5y ago
    They might have wondered it already. And even asked, “why are we doing this? Seems like a bad idea.” But when the response is a list of reasons that may or may not be good, you just go with it. All of this was done with intention.
- lrem 5y ago
  Well, it wouldn't prevent that one user who requested the feature. But other users would be made aware that their logging facility now does surprising new things.
- light_hue_1 5y ago
  Haskell could and would absolutely prevent this problem. Haskell does not work by aggregating together the features that a whole system needs. It works by breaking down permissions per function. You would immediately see that a function which was only ever meant to do context lookups also has network access. This would be such a crazy type for such a simple function that no one would write it this way. Don't think about it as aggregating effects, think about it as, all of the leaves of the system have the most narrow permissions possible. And that's where most bugs are, in the leaves.
  - MichaelBurge 5y ago
    If I were writing Haskell logging functions, I would use the type "String -> IO ()" and it could do whatever it wanted including network access. I might distinguish resolveFormatString :: String -> [List Parameter] -> IO String" resolveFormatStringSafe :: String -> [List Parameter] -> String but it wouldn't be "most narrow permissions possible". It would be "everything or nothing".
    - light_hue_1 5y ago
      You would never spot this the edge of the logging API. In any case, it's easy to see this can't be the right mental model for security in Haskell. main is `IO Int` so at a gross level you can't say anything about an API or a program. Security in Haskell is about internal guarantees. The developers of the library would immediately spot that their call does a lot more than it was ever supposed to locally. They would have a function that has a crazy permissive type like IO instead of something very narrow related to the specific functionality they need to do their one lookup.
      - chii 5y ago
        > The developers of the library would immediately spot that their call does a lot more than it was ever supposed to locally but the point was that if the feature is intentionally developed, then the type signatures would reflect it - it doesn't do "a lot more than it was ever supposed to". Type systems don't tell you that a logging library shouldn't access the network. It just tells you that it does, and if this feature was intentional, then how would the type system flag it differently from a cURL-like library that writes to disk with data from the network?
griffinmb 5y ago
Effects can definitely help, but a strong type system allows you to encode security concerns for compile time feedback as well. See https://gmb.is/refinement-types.html https://gmb.is/refinement-types.html for a non-Haskell example.
- Quekid5 5y ago
  For a much simpler example: newtypes can make enforcing proper escaping[0] completely trivial and checked by the compiler. It's very similar to tainted values in Perl except enforced at compile time. [0] No, not sanitization!
marcosdumay 5y ago
The log4j thing was a feature very specific to the Java culture. It very likely wouldn't happen in Haskell, but probably wouldn't happen in Python or C either. In Haskell, effectful text parsing is severely frowned upon, so that template language wouldn't get used there. In Python people would frown upon the multi-use function that runs a template engine and logs text when those should be 2 functions. In C people would be up in arms over a logging framework that doesn't log exactly the text you gave it.
- pjmlp 5y ago
  You mean the same set of people that a decade earlier were doing the same architecture designs in C, C++, Smalltalk, with help of DCE, CORBA and COM? In C you would be playing with lots of interesting macros at enterprise level scale, doing Sun RPC calls, encoded in ASN.1, and maybe even manually twerking the generated stubs.
tlavoie 5y ago
One area that I think Haskell (and some other languages) are good in security terms, is that the functionality present when deployed is pretty much all you're going to get. What I mean by this is that you're not tempted to use some arbitrary eval() method on untrustworthy input, nor are you likely to be able to just start reading and running code found some place on disk from a binary-installed app. The main log4j vuln that's caused an uproar wasn't just that it did some sort of dynamic lookup at run-time, but also that it could then take the result, and run it as attacker-controlled bytecode. Similarly, a web application that uses say, Python or PHP might have an exploitable vulnerability where the user can upload files. That functionality is going to be intentional, but the problem can crop up that the user can control the upload path, and the application can then execute the uploaded file. Other vulnerabilities can certainly be written in Haskell, but remote code execution (RCE) vulnerabilities are the sort of jackpot issue that will be much more difficult to pull off there. The same should apply to most languages with a distinct dev-time compilation step, as long as they've got other memory safety controls. (Rust, Go, Ocaml are likely fine as well for instance.)

lelanthran 5y ago

> I have the feeling that Haskell has one feature that could be super useful for security. > > That feature is the explicit typing of effects via monads. Just look at the recent log4j example: If effects were explicitly typed in Java, you would potentially scratch your head why you need a network monad or a "insert code into the process" effect to just log a line. That would not have helped - the network access with RCE was a feature put into the library. What does the language selection have to do with a feature request of "We want evaluated log strings to be able to do network access with RCE"? There's nothing special in any language (even Haskell) that will prevent this sort of thing.

Buttons840 5y ago
> What does the language selection have to do with a feature request of Only functions with certain type signatures can do IO in Haskell. This could be broken down to be more granular such that the type system makes it clear (and even somewhat of a burden) to the caller whether writing to disk happens, or network access, or both. Imagine the entry point to your program is given all "Effects", and then must pass them down the call stack as needed to other functions. Without the appropriate Effect, a function cannot perform the Effect. People might wonder why they were required to pass the NetworkAccess Effect into their logging calls.
- stonemetal12 5y ago
  Let's just hope there is a "load and execute random code from the network" effect that you could disable. NetworkAccess Effect wouldn't be that strange for a logging system that supports multiple networked log managers like syslog.
  - Quekid5 5y ago
    The point isn't so much that you can disable effects. It's that you literally have no effects/capabilities unless specifically granted. That said, I'm a bit skeptical that Haskell would have prevented this particular issue in practice. The logging monad would just likely just have been called a LoggingM (in MTL style) and most users would have been oblivious as to exactly what it was doing... and as you say: Logging to a remote system needs the network. I guess what could have saved a Haskell program here is that there's no such thing as "download code and execute it with the same privileges as you" with being very explicit about that. (E.g. calling 'system' or whatever)
    - Akronymus 5y ago
      You could split it up into 2 functions I guess. A pure one that creates the log entry, then an IO one that actually saves it.
      - Quekid5 5y ago
        Yes, but if the IO one does <shenanigans> then you're as well off. Which is... not very. EDIT: Just to say: I don't mean to be flippant.
        Akronymus 5y ago
        Oh its fine. And i meanr it more in that one part is literally just passing the data along, while the other part generates the data with being fed whatever is needed for it to. so, if yoj want to just log a literal string yoj wouldnt provide any additional functionality to the generator. if you want it to expand strings, then you provide a function for that. and so on
griffinmb 5y ago
The point is that with a powerful Effects system, devs calling the logger would have to account for the network call in their own code. Someone might have wondered why that was needed and gotten this addressed before it was ever widespread.
- lelanthran 5y ago
  > The point is that with a powerful Effects system, devs calling the logger would have to account for the network call in their own code. Someone might have wondered why that was needed and gotten this addressed before it was ever widespread. No one would have wondered anything - it's a networked logger, with network functionality.
- inkeddeveloper 5y ago
  They might have wondered it already. And even asked, “why are we doing this? Seems like a bad idea.” But when the response is a list of reasons that may or may not be good, you just go with it. All of this was done with intention.
lrem 5y ago
Well, it wouldn't prevent that one user who requested the feature. But other users would be made aware that their logging facility now does surprising new things.
light_hue_1 5y ago
Haskell could and would absolutely prevent this problem. Haskell does not work by aggregating together the features that a whole system needs. It works by breaking down permissions per function. You would immediately see that a function which was only ever meant to do context lookups also has network access. This would be such a crazy type for such a simple function that no one would write it this way. Don't think about it as aggregating effects, think about it as, all of the leaves of the system have the most narrow permissions possible. And that's where most bugs are, in the leaves.
- MichaelBurge 5y ago
  If I were writing Haskell logging functions, I would use the type "String -> IO ()" and it could do whatever it wanted including network access. I might distinguish resolveFormatString :: String -> [List Parameter] -> IO String" resolveFormatStringSafe :: String -> [List Parameter] -> String but it wouldn't be "most narrow permissions possible". It would be "everything or nothing".
  - light_hue_1 5y ago
    You would never spot this the edge of the logging API. In any case, it's easy to see this can't be the right mental model for security in Haskell. main is `IO Int` so at a gross level you can't say anything about an API or a program. Security in Haskell is about internal guarantees. The developers of the library would immediately spot that their call does a lot more than it was ever supposed to locally. They would have a function that has a crazy permissive type like IO instead of something very narrow related to the specific functionality they need to do their one lookup.
    - chii 5y ago
      > The developers of the library would immediately spot that their call does a lot more than it was ever supposed to locally but the point was that if the feature is intentionally developed, then the type signatures would reflect it - it doesn't do "a lot more than it was ever supposed to". Type systems don't tell you that a logging library shouldn't access the network. It just tells you that it does, and if this feature was intentional, then how would the type system flag it differently from a cURL-like library that writes to disk with data from the network?

griffinmb 5y ago

Effects can definitely help, but a strong type system allows you to encode security concerns for compile time feedback as well. See https://gmb.is/refinement-types.html https://gmb.is/refinement-types.html for a non-Haskell example.

Quekid5 5y ago
For a much simpler example: newtypes can make enforcing proper escaping[0] completely trivial and checked by the compiler. It's very similar to tainted values in Perl except enforced at compile time. [0] No, not sanitization!

marcosdumay 5y ago

The log4j thing was a feature very specific to the Java culture. It very likely wouldn't happen in Haskell, but probably wouldn't happen in Python or C either. In Haskell, effectful text parsing is severely frowned upon, so that template language wouldn't get used there. In Python people would frown upon the multi-use function that runs a template engine and logs text when those should be 2 functions. In C people would be up in arms over a logging framework that doesn't log exactly the text you gave it.

pjmlp 5y ago
You mean the same set of people that a decade earlier were doing the same architecture designs in C, C++, Smalltalk, with help of DCE, CORBA and COM? In C you would be playing with lots of interesting macros at enterprise level scale, doing Sun RPC calls, encoded in ASN.1, and maybe even manually twerking the generated stubs.

tlavoie 5y ago

One area that I think Haskell (and some other languages) are good in security terms, is that the functionality present when deployed is pretty much all you're going to get. What I mean by this is that you're not tempted to use some arbitrary eval() method on untrustworthy input, nor are you likely to be able to just start reading and running code found some place on disk from a binary-installed app. The main log4j vuln that's caused an uproar wasn't just that it did some sort of dynamic lookup at run-time, but also that it could then take the result, and run it as attacker-controlled bytecode. Similarly, a web application that uses say, Python or PHP might have an exploitable vulnerability where the user can upload files. That functionality is going to be intentional, but the problem can crop up that the user can control the upload path, and the application can then execute the uploaded file. Other vulnerabilities can certainly be written in Haskell, but remote code execution (RCE) vulnerabilities are the sort of jackpot issue that will be much more difficult to pull off there. The same should apply to most languages with a distinct dev-time compilation step, as long as they've got other memory safety controls. (Rust, Go, Ocaml are likely fine as well for instance.)