12 ms·

Leveraging the type system to avoid mistakes

167 points by amzans 8y ago

oherrala 8y ago
I wrote about the same topic in https://medium.com/sensorfu/using-static-typing-to-protect-against-code-injection-attacks-353002ca6f2b https://medium.com/sensorfu/using-static-typing-to-protect-a... Type systems are really good in helping to avoid this problem!
tetha 8y ago
Another interesting and, retrospectively, obvious idea I recently read about: Have a class 'CleartextPassword' around, which overrides all string-serialization as either a sequence of *s, or a hashcode of the password. Suddenly the type system prevents security issues.
- 49bc 8y ago
  Cool idea. However It’s the DB that usually leaks the password, not the stack* Assuming we’re talking about Scala and not C.
  - pdpi 8y ago
    The issue isn't the stack, but rather an errant printf() or log() call — presumably, something like this would help with the issues that Twitter had recently. https://www.theverge.com/2018/5/3/17316684/twitter-password-bug-security-flaw-exposed-change-now https://www.theverge.com/2018/5/3/17316684/twitter-password-...
    - tzahola 8y ago
      I’m pretty sure the Twitter fiasco was some sort of trace logging that logged every request body, and some of those requests happened to contain passwords. Introducing a separate type for passwords doesn’t solve this issue.
      - staticassertion 8y ago
        Whatever the type was, it contained a password, and therefor could have been moved into a type that prevented the bug. Whether it's a password or an "unparsed client data" structure or whatever.
        tetha 8y ago
        This is going to be even more interesting if the EU keeps pushing privacy laws. Are you even allowed to trace productive unrestricted HTTP calls anymore? I find this exciting from a problem-solving point of view, because for one, this is potentially a hard, ground-shifting problem. And on the other hand, languages like scala, haskell or rust have the tools to make this kind of requirements simple. There's an interesting time coming.
    - tetha 8y ago
      Exactly. Such a class doesn't secure the entire multi-container / multi-vm setup of a clustered web application, how could it? However, this is a simple layer of defense in depth, since it makes it harder for your application code to accidentally log out passwords. And in a language with deconstructors, you can remove the secret from memory after it has been used. This in turn reduces the window of vulnerability against memory disclosure attacks, especially in shared virtualized environments.
- Gibbon1 8y ago
  I've though would be nice if languages had a 'secure' type qualifier which prevents leakage when something goes out of scope. AKA, compiler will issue code to zero out the data in memory once it's out of scope. Extending that, passing a secure type to an insecure function should result in a warning at least. log_printf( password.cleartext()); // error log_printf( password.safehash()); // okay
  - sigfubar 8y ago
    Such real-world concerns can and should be modeled using types. Your comment reminded me of taint mode in Perl. https://perldoc.perl.org/perlsec.html#Taint-mode https://perldoc.perl.org/perlsec.html#Taint-mode
    - Gibbon1 8y ago
      Not sure if types will force the compiler to do things like constant time comparisons and overwrite sensitive information as it goes out of scope. I think Java, C#, and C/C++ the compiler will decide that code to clear memory just before it goes out of scope has no side effects and optimize that code away.
      - zenhack 8y ago
        You can definitely rig up the erasure to happen in a destructor (C++) or Drop implementation (Rust). Convincing the compiler not to optimize it out is tricky, but many cryptographic libraries include that functionality. The c11 standard has a memset_s function with the right semantics, but there are other ways to implement it. Re: constant time operations, I don't know of any language or system that does this currently. But a while back I was kicking around the idea with a friend and we came to a design that I'm pretty sure would work. Never got around to implementation though; so many projects, so little time.
      - chriswarbo 8y ago
        We can absolutely use types to ensure that our algorithms are constant time, e.g. https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida https://www.usenix.org/conference/usenixsecurity16/technical... We can use types to enforce the big-O runtime of our functions too, e.g. ensuring that a mergesort implementation runs in O(nlogn) steps: https://www.twanvl.nl/blog/agda/sorting https://www.twanvl.nl/blog/agda/sorting I have no idea about doing these things in Java/C/C++/C# though; anything we try to enforce can be trivially broken by `NULL` :(
- Rapzid 8y ago
  Scott Wlaschin, of fsharp for fun and profit, has written/presented[1] quite a bit about utilizing the type system to prevent invalid states. Diff lang, but sim concepts. It was an epiphany to me and a concept I have at least tried to bring back to the ALGOL side where possible. [1]https://fsharpforfunandprofit.com/series/designing-with-types.html https://fsharpforfunandprofit.com/series/designing-with-type...
  - jackweirdy 8y ago
    This reminds me of an article by Foursquare about how they use Scala Phantom Types to ensure MongoDB queries are semantically well formed: https://engineering.foursquare.com/going-rogue-part-2-phantom-types-d18ece7235e6 https://engineering.foursquare.com/going-rogue-part-2-phanto...
- danpalmer 8y ago
  The other great motivating example I’ve seen is an Amount type parametrised by currency as well as the numerical value, so that the type system can enforce that you don’t add two amounts of different currencies, or that to add, you have to also provide a correctly typed exchange rate value.
bgirard 8y ago
I suggested a similar trick in Gecko when we were seeing too many bugs in the rendering/async scrolling code because of mistakes when transforming between the different unit spaces: https://dxr.mozilla.org/mozilla-central/rev/4303d49c53931385892231969e40048f096b4d4c/layout/base/Units.h#385-465 https://dxr.mozilla.org/mozilla-central/rev/4303d49c53931385... Transformations between units are also typed so you wont accidentally use the wrong scale factor when transforming.
- Gibbon1 8y ago
  Working on porting code with time units that are totally unspecified. Sometimes it's seconds, ms, 1/256th of a second or HH:MM:SS. Just shoot me.
  - insulanian 8y ago
    You need F#'s units of measure [1]. [1] https://fsharpforfunandprofit.com/posts/units-of-measure/ https://fsharpforfunandprofit.com/posts/units-of-measure/
dfan 8y ago
I have a system set up in C++ to make it trivial to add new unique kinds of IDs (wrappers around ints) as well as vectors that can be indexed only with that kind of ID. So you can have a ShoeVec containing Shoes that is indexable only by ShoeIDs and a ShirtVec containing Shirts that is indexable only by ShirtIDs. It's zero-overhead in optimized builds, of course. You'd be surprised how rarely you have to convert to or from the underlying type.
- jdonaldson 8y ago
  Fwiw the Haxe language calls this an "abstract type", and they're very useful. https://haxe.org/manual/types-abstract.html https://haxe.org/manual/types-abstract.html
  - deleted 8y ago
    [deleted]
  - rurban 8y ago
    Generic types are useful, but still should be called as such, or for the new fad: dependent types. Abstract types would not allow instantiation.
    - jdonaldson 8y ago
      Haxe abstract types are distinct from abstract classes, but I need to learn more about dependent types.
- kazinator 8y ago
  Congrats, you almost have Pascal there.
jph 8y ago
The article's example boils down to this pseudocode: function foo(s, i) { s * i } s = "hello" i = 2 foo(i, s) // BUG. The runtime crashes. The article advocates adding a type system to detect the bug: function foo(String str, Integer int) { s * i } String s = "hello" Integer i = 2 foo(i, s) // BUG. The compiler detects the error. If you're interested in these kinds of errors, then you may also want to consider ideas such as named parameters: function foo(text: s, count: i) { s * i }
- amzans 8y ago
  The problem with named parameters is that you can theoretically still pass the wrong value, and in practice not everyone is using named parameters on every function call. By relying on the type system you can catch that issue at compile time and not have to worry about it. We use this technique at work when there’s lots of fields in our data types as it’s nice to be able to keep track of the types during all the transformations and to avoid subtle bugs. Specially as the codebase is constantly changing.
  - jph 8y ago
    I agree with you. My opinion is that type checking helps, and so do assertions, borrow checkers, pen testers, etc. The tradeoff IMHO is that these take some time and thought to do well. Would you be willing to send me an example of your best-case for using a type system? For example some code where you feel the type system really helps you and your team? I keep a log of these real world areas, for training my teams. Anonymized code is fine. My email is joel@joelparkerhenderson.com. Thank you!
  - tayo42 8y ago
    Do you do this for every string, int, float etc..? Any downsides you run into? I always thought it would be interesting to try it using a type even if it wraps something but never had tried going all in on the idea. In scala do you not use alias ever? I guess they don't help much? Alias of strings can be used interchangeably I think?
    - 8y ago
amzans 8y ago
Something that I enjoy very much in Scala is sealed traits + case classes. sealed trait Food case class FishTaco(size: FishSize) extends Food case class Burger(numPatties: Int) extends Food case class Spaghetti(sauce: PastaSauce) extends Food It’s like Enums + Data Classes on steroids. You can pass around and transform your data as usual, but if you forgot to handle a specific case when doing pattern matching you’ll get a compile warning. For example in the following case: input match { case Burger(patties) => ... case Spaghetti(sauce) => ... } The compiler will happily yell at you something like: warning: match may not be exhaustive. It would fail on the following input: FishTaco(_) Little things such as this one help reasoning about your program since you can rely on the types describing what is possible and what is not.
- deleted 8y ago
  [deleted]
- Rapzid 8y ago
  If you like that kinda thing you should check out F# as well. The IDE experience/speed is much better for F# IMHO, but I have a lot of respect for the concepts behind both. And of course they ride on completely separate massive ecosystems, so you can't exactly swap them out willy-nilly.. I wish I could figure out why my IDE experience with Scala and IntelliJ(IDEA) was so darn sluggish. Also hoping they jump on the language server protocol bandwagon in the future.
  - brianberns 8y ago
    Yep, these are called "discriminated unions" in F#. I think most functional programming languages have something similar. The underlying concept is "algebraic data types": You can compose types as products (tuples or records) and sums (discriminated unions) of simpler types. From there, you can actually use algebra on types, which is pretty mind-blowing. For example, we can define a generic sum type called Either: Either a b = Left a | Right b You can think of Either as the sum of types "a" and "b": a + b. Tuples are product types, so you can use the distributive property of multiplication over addition to establish that: (a, Either b c) = Either (a, b) (a, c) Or algebraically: a * (b + c) = (a * b) + (a * c) This is one of those areas where category theory is actually useful for programmers.
grosjona 8y ago
The problem with complex type systems is that they force you to spend a lot of your development time thinking about type structures and their relationships (in a universal way) instead of thinking about actual logic (in a more localized way). For example, when you introduce third party modules into your code, sometimes it's impossible to cleanly reconcile the type structures exposed by the module with the type structures within your own system... You may end up with essentially identical concepts being classified as completely different types/classes/interfaces... It creates an unnecessary impedance mismatch between your logic and the logic exposed by third-party modules. This type impedance mismatch may discourage developers from using third-party modules altogether. That might explain why dynamically typed languages like JavaScript and Ruby have such rich third-party module ecosystems compared to that of statically typed languages. Unless there is a single standardized and universally accepted type system which is fully consistent across the minds of all developers of a specific language/platform (for all possible applications), then a type system makes no sense at all; especially a complex one.
- whateveracct 8y ago
  Those impedance mismatches are equally present in dynamically typed code. The only thing types do is help make it obvious when there are problems with composition. I work in Haskell with many other Haskell developers and a wide variety of Haskell mindsets. It’s a very complex type system we use a lot of, and so far, the issues you mention are so minor and worth it.
  - grosjona 8y ago
    With dynamically languages, the type of an object is not important so you don't need to explicitly typecast external objects to fit into your logic. With dynamically typed languages, if two different objects expose the same functions then you can use them in the same way. The behavior of an object is all that counts.
    - wtetzner 8y ago
      You seem to be talking about nominal types being a problem. Structural subtyping and row types are two ways of getting the benefits you're talking about while still being statically typed.
49bc 8y ago
I’m seeing a little bit of a waterbed effect here. The author has replaced the basic type with one that matches it in name. You will never accidentally send CustomerId to CartID because the compiler will fail... but now we’ll nees to dig through the code to find out whether customer ID should be an int, int32, String.... what the heck is it anyway? In scala can I not just say foo(item1=item1) even if foo takes only 1 arg?
- tytytytytytytyt 8y ago
  > In scala can I not just say foo(item1=item1) even if foo takes only 1 arg? Why would you want to do that? That's less succinct than foo(item1). What are you really asking?
- amzans 8y ago
  Usually you would lookup the definition of those types just as you do for the function that you are trying to call. At least it’s a good idea to know what a function accepts before passing around your customer IDs ;) And to answer your last question, yes in Scala you can use named parameters like in your example.
lihaoyi 8y ago
I wrote a blog post that goes into a lot more detail into some of these techniques, in case anyone wants to dive deeper - http://www.lihaoyi.com/post/StrategicScalaStylePracticalTypeSafety.html http://www.lihaoyi.com/post/StrategicScalaStylePracticalType... - http://www.lihaoyi.com/post/StrategicScalaStyleDesigningDatatypes.html http://www.lihaoyi.com/post/StrategicScalaStyleDesigningData...
andreygrehov 8y ago
I believe a lot of similar concepts are explained in Domain Driven Design.
GavinMcG 8y ago
This got me thinking, and I'm curious what a language would look like if basic types weren't directly usable. In other words, maybe type checking doesn't go far enough: checking that I'm getting an int is less valuable than checking that I'm getting the right sort of data for the domain.
- daxfohl 8y ago
  unsigned int?
- tzahola 8y ago
  See Boost.Units: https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.html https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.h... It enforces correct units/dimensions at compile time, so you won’t be able to mix up length with time or area, etc.
- ghayes 8y ago
  This might be a good time to check out algebraic data types, esp. with a single constructor. For example, in Elm you might declare: type Length = Inches Int Then any function that accepts a Length, you can only pass in a length. This effectively acts like tagged tuples verified at compile time. You can later extend this type to be: type Length = Inches Int | Meters Int and any code that reads length would have to handle both cases (also checked at compile that). I have found this to be a great way of ensuring all of your types are correct (and sometimes, a great frustration of wishing I didn't have to wrap/unwrap types so often).
  - GavinMcG 8y ago
    Yeah, that's one of my favorite takeaways from Elm. I'm thinking of it in an OO style, where perhaps instead of wrapping/unwrapping you're specifying an analog to object properties.
  - insulanian 8y ago
    F# has units of measure [1], which are very nice for such a case you're describing. [1] https://fsharpforfunandprofit.com/posts/units-of-measure/ https://fsharpforfunandprofit.com/posts/units-of-measure/
tzahola 8y ago
Even though people love bashing Objective-C for its “weird” method syntax, it trivially circumvents these kind of problems. Also related: Mike Ash’s post about using single-member C structs instead of unitless scalar types: https://www.mikeash.com/pyblog/friday-qa-2013-08-02-type-safe-scalars-with-single-field-structs.html https://www.mikeash.com/pyblog/friday-qa-2013-08-02-type-saf...
platz 8y ago
Make illegeal states unrepresentable
CharlesMerriam2 8y ago
There is often an I love {Scala|Rust|Erland} post showing an simple type issue and claiming that using a bunch of new syntax would somehow fix it. <rant> 1. I want a minimum of typed syntax for safety. For example, remember Hungarian Notation? My linter barfs if I try "icCart = ipMyProduct" because of the semantic type issue. 2. I want a full set of primitives. For example, counts (c) are 0 or above, not infinite, can do arithmetic) while ids (i) are positive, not infinite, cannot do arithmetic, cannot assign constant). I want optionals; I want clearer error handling; I want fully declared I/O instead of manual error handling; I want better. 3. I want tallies of how often simple types are confused before changing languages to fix. My type confusions are complicated nested collections or variant records. </rant> Typing is a means for correct programming, not an end in itself.
- jpitz 8y ago
  >Typing is a means for correct programming, not an end in itself. That's not always the case. https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview
hardwaresofton 8y ago
If you like this, you're probably also going to like Haskell/OCaml/Ada/F#/Coq (ML family of languages?): I'll leave links for Haskell since the only one of those I've tried and liked personally: https://www.haskell.org/ https://www.haskell.org/ http://learnyouahaskell.com/ http://learnyouahaskell.com/ IMO Haskell is the type system you wanted Java to have, with even more strictness. While it's possible to write unsafe haskell, just about everything you will read, and the language itself encourages you to push as many worries as you can to be solved by the type system. If that doesn't get you excited, there's actually a saying that is mostly true in my experience writing Haskell -- "If it compiles, it works"(tm). Also Haskell on the JVM if you want to dip your toes in: - https://eta-lang.org/ https://eta-lang.org/ - https://github.com/Frege/frege https://github.com/Frege/frege [EDIT] - If you try to learn haskell you'll inevitably run into the M word which rhymes with Gonad. The best guide I've ever read is @ http://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_pictures.html http://adit.io/posts/2013-04-17-functors,_applicatives,_and_... BTW, be ye warned: when you start understanding/getting cozy with the concepts introduced by Haskell you'll wish they were everywhere, and they're not. Languages without proper union types will look dumb to you, easy function composition/points free style will be a daily desire, and monadic composition of a bunch of functions will be frustratingly absent/ugly in other languages, not doing errors-as-values will look ironically error-prone. [EDIT 2] - More relevant to the actual post, how you would do this in Haskell is using the `type` keyword (type aliasing, e.g. `type Email = String`) or the `newtype` keyword, which creates a new type that is basically identical (what the article talks about). Here's some discussion on newtype: - http://degoes.net/articles/newtypes-suck http://degoes.net/articles/newtypes-suck (this article is good, it describes the premise, promise, shortcomings, and workarounds, forgive the clickbaity title) - https://www.reddit.com/r/haskell/comments/4jnwjg/why_use_newtype/ https://www.reddit.com/r/haskell/comments/4jnwjg/why_use_new...
- Silhouette 8y ago
  Although Haskell has a relatively powerful and useful type system, you are perhaps being a little kind to it here. Haskell also has partial functions, including quite a few dangerous examples in the standard library, various mechanisms to escape the type system entirely, and 27 different ways to handle errors, 28 of which look a bit like exceptions but need handling in 29 different ways. And it still can't handle basic record types very elegantly, nor dependent types such as fixed-size arrays/matrices. Haskell's type system does have a lot going for it and it also makes a useful laboratory for experiments with type-based techniques, but as far as safety goes it has never really lived up to the hype, and for all its advanced magic, it is surprisingly lacking in support for some basic features that are widely available in other languages.
hzhou321 8y ago
The suggested type system adds a lot of code and complexity. For the specific case, I suggest we can try a convention-based solution. Let's, eg. establish a convention that all product id variable named with `prod_` prefix and customer id variable named with `cust_` prefix. Then a simple static analyzer filter can serve as the unit test to catch mistakes (include passing in variable names that don't conform the convention). We should recognize that the enforced prefix serves the same role as the type system but at the preprocessing stage rather than the compiler stage. It does not require the programmer to add any extra code; rather it helps one of the difficult problems of naming things. Unlike the type system, it is easy to adopt strong convention (the strongest being a set of fixed names) and then relax the convention as the program evolves. In contrast, the type system often takes the opposite path of from relax to strict with steep increasing cost. Of course, unlike the type system, the enforcement of the convention does not come automatically -- the programmer has to write static analysis code to enforce it -- this is fundamentally not different from writing unit tests. But the static analysis code is easy to write and less likely to have bugs (and bugs have less severe consequences). I use a general purpose preprocessor, MyDef, and every line of my code goes through several places of filtering anyway, so adding a set of static checks seem trivial. But even you don't use a preprocessor, implementing a simple static convention checker (to be enforced at repository check-in) doesn't seem difficult.
- nine_k 8y ago
  > unlike the type system, the enforcement of the convention does not come automatically This defeats the whole purpose. > the programmer has to write static analysis code It is legwork that should be relegated to the computer. And, in fact, has been for a long time. I don't only mean type systems; various linters and checkers work where the compiler proper does not (see valgrind or findbugs). Frankly, a lot of test cases for code can be written automatically; the prime example is Haskell's QuickCheck, but a number of other languages has similar tools, all the way down to fully dynamic ones like Python.
  - hzhou321 8y ago
    Creating and maintain type system is also leg walk (and I was arguing it is a bigger burden of leg walk). And a Turing complete type system can have Turing complete errors. Let's not pretend we have silver bullet and have a fair discussion
dclowd9901 8y ago
What really put me on to typing JavaScript was this. The ability to avoid unit tests. And frankly what unit test would ever even capture something like this, an implementation issue, (unless you refactored a lib).
- clintonb 8y ago
  > Don’t get me wrong I’m not saying to scrap all your test suites and try to encode all your constraints using the type system instead. Not at all I still firmly believe that tests are useful but in some cases you can leverage the type system to avoid mistakes. You should still write unit tests. You should also write integration/functional tests that might have caught this error when you tested the code that calls the function in question. The only scenario I can see the argument swapping bug not being caught is when all of the ID arguments equal the same value.
dnomad 8y ago
Types can definitely help with data well-formedness but personally I'm very suspicious of 'mini-types' like Name and CartID. If the data you're wrapping has no internal structure (that can be formally verified) and you're just using the type system as an argument checker then it's not clear to me that you're really adding much value. If CartID and ProductID are both just strings what's to stop a user from doing the same as: CartID cartId = new CartID(productId.toString()); addToCart(..., cartId, ...); <-- but look that's really a ProductID! I'd suggest that while you may have reduced the likelihood of certain errors you have not actually eliminated those errors. The right approach here is to be very suspicious of any methods in your domain that just take a bunch of IDs. Either: (a) Force the caller to resolve the IDs to actual entities before invoking the method: addToCart(Cart c, Product p, ...) or (b) Represent the method parameters as a Parameters object or, preferrably, an Event object. handle(ProductAddedEvent event); The real problem here is not the type system but a domain that is not sufficiently protected by an Anti-Corruption Layer [1]. Unfortunately most developers are not familiar with this kind of strategic design and languages are not much help here. It would be interesting if there was a language that could flag things like weak ACLs. [1] https://docs.microsoft.com/en-us/azure/architecture/patterns/anti-corruption-layer https://docs.microsoft.com/en-us/azure/architecture/patterns...
- gcommer 8y ago
  > new CartID(productID.toString()); With good data modeling and safety checks, this should fail: a product id and cart id should have some sort of distinguishing syntax (eg "P1234" vs "C1234") and so `new CartID("P1234")` will fail. At some point, no sorts of type system can stop incorrectly implemented/specified logic. An even simpler example would be just passing some constant, valid, but not semantically correct string to the CartID constructor. Your (a) and (b) solutions don't solve this. I could just as easily create a meaningless Cart object, or a meaningless ProductAddedEvent the same way you constructed that meaningless CartID.
  - dnomad 8y ago
    As I said, if your data actually has internal structure that can be verified then the Type is meaningful. (Though that sort of prefixing introduces its own problems and I think most IDs just end up being UUIDs or URIs or numbers.) Otherwise you're just wrapping strings. The point here is that a Type represents data and behavior or, more formally, Types represent constraints over a space of data and behavior. Types that don't actually do any constraining are useless. > I could just as easily create a meaningless Cart object, or a meaningless ProductAddedEvent the same way you constructed that meaningless CartID. The problem here is not mixing up IDs. The problem is actually guaranteeing that the pre-conditions of addToCart() have been satisfied. Here, for example, addToCart() probably wants more than just a Cart and Product object, but a Cart and Product objects that have been persisted. Presumably the domain has been constrained so that you can't create meaningless objects. Otherwise what's the point of any object? If the only valid Cart and Product objects are those that can be retrieved from a persistent repository then, yes, this not only solves the trivial problem of mixing up IDs, but also the more valuable underlying problem that addToCart() is constrained to act on real, valid (according to the domain) Cart and Product objects. In other words, this isn't really an issue of language design. And while there's a tendency to believe the language can solve every problems and that design patterns are a sign of language "weakness" the reality is developers that really want to solve these problems will have to think carefully about their domain and apply the appropriate design patterns.
billfruit 8y ago
One thing that I personally would find useful is a F# like Unit of Measure, kind of type metadata, that allows units of quantities to be explicitly mentioned, and there by help in preventing unit confusions in code, ie passing around values in the wrong kind of units, esp degrees and radians for eg, can often be a difficult mistake to catch.
thankthunk 8y ago
Leverage the type system? Type systems exists to allow you catch errors at compile time. That is what it's there to do. It's like saying leveraging the compiler to compile or leveraging the cup to drink water.
rurban 8y ago
The id type parameter is not called phantom type, it's called generic type.

167 points by amzans 8y ago

I wrote about the same topic in https://medium.com/sensorfu/using-static-typing-to-protect-against-code-injection-attacks-353002ca6f2b https://medium.com/sensorfu/using-static-typing-to-protect-a... Type systems are really good in helping to avoid this problem!

tetha 8y ago

Another interesting and, retrospectively, obvious idea I recently read about: Have a class 'CleartextPassword' around, which overrides all string-serialization as either a sequence of *s, or a hashcode of the password. Suddenly the type system prevents security issues.

49bc 8y ago
Cool idea. However It’s the DB that usually leaks the password, not the stack* Assuming we’re talking about Scala and not C.
- pdpi 8y ago
  The issue isn't the stack, but rather an errant printf() or log() call — presumably, something like this would help with the issues that Twitter had recently. https://www.theverge.com/2018/5/3/17316684/twitter-password-bug-security-flaw-exposed-change-now https://www.theverge.com/2018/5/3/17316684/twitter-password-...
  - tzahola 8y ago
    I’m pretty sure the Twitter fiasco was some sort of trace logging that logged every request body, and some of those requests happened to contain passwords. Introducing a separate type for passwords doesn’t solve this issue.
    - staticassertion 8y ago
      Whatever the type was, it contained a password, and therefor could have been moved into a type that prevented the bug. Whether it's a password or an "unparsed client data" structure or whatever.
      - tetha 8y ago
        This is going to be even more interesting if the EU keeps pushing privacy laws. Are you even allowed to trace productive unrestricted HTTP calls anymore? I find this exciting from a problem-solving point of view, because for one, this is potentially a hard, ground-shifting problem. And on the other hand, languages like scala, haskell or rust have the tools to make this kind of requirements simple. There's an interesting time coming.
  - tetha 8y ago
    Exactly. Such a class doesn't secure the entire multi-container / multi-vm setup of a clustered web application, how could it? However, this is a simple layer of defense in depth, since it makes it harder for your application code to accidentally log out passwords. And in a language with deconstructors, you can remove the secret from memory after it has been used. This in turn reduces the window of vulnerability against memory disclosure attacks, especially in shared virtualized environments.
Gibbon1 8y ago
I've though would be nice if languages had a 'secure' type qualifier which prevents leakage when something goes out of scope. AKA, compiler will issue code to zero out the data in memory once it's out of scope. Extending that, passing a secure type to an insecure function should result in a warning at least. log_printf( password.cleartext()); // error log_printf( password.safehash()); // okay
- sigfubar 8y ago
  Such real-world concerns can and should be modeled using types. Your comment reminded me of taint mode in Perl. https://perldoc.perl.org/perlsec.html#Taint-mode https://perldoc.perl.org/perlsec.html#Taint-mode
  - Gibbon1 8y ago
    Not sure if types will force the compiler to do things like constant time comparisons and overwrite sensitive information as it goes out of scope. I think Java, C#, and C/C++ the compiler will decide that code to clear memory just before it goes out of scope has no side effects and optimize that code away.
    - zenhack 8y ago
      You can definitely rig up the erasure to happen in a destructor (C++) or Drop implementation (Rust). Convincing the compiler not to optimize it out is tricky, but many cryptographic libraries include that functionality. The c11 standard has a memset_s function with the right semantics, but there are other ways to implement it. Re: constant time operations, I don't know of any language or system that does this currently. But a while back I was kicking around the idea with a friend and we came to a design that I'm pretty sure would work. Never got around to implementation though; so many projects, so little time.
    - chriswarbo 8y ago
      We can absolutely use types to ensure that our algorithms are constant time, e.g. https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida https://www.usenix.org/conference/usenixsecurity16/technical... We can use types to enforce the big-O runtime of our functions too, e.g. ensuring that a mergesort implementation runs in O(nlogn) steps: https://www.twanvl.nl/blog/agda/sorting https://www.twanvl.nl/blog/agda/sorting I have no idea about doing these things in Java/C/C++/C# though; anything we try to enforce can be trivially broken by `NULL` :(
Rapzid 8y ago
Scott Wlaschin, of fsharp for fun and profit, has written/presented[1] quite a bit about utilizing the type system to prevent invalid states. Diff lang, but sim concepts. It was an epiphany to me and a concept I have at least tried to bring back to the ALGOL side where possible. [1]https://fsharpforfunandprofit.com/series/designing-with-types.html https://fsharpforfunandprofit.com/series/designing-with-type...
- jackweirdy 8y ago
  This reminds me of an article by Foursquare about how they use Scala Phantom Types to ensure MongoDB queries are semantically well formed: https://engineering.foursquare.com/going-rogue-part-2-phantom-types-d18ece7235e6 https://engineering.foursquare.com/going-rogue-part-2-phanto...
danpalmer 8y ago
The other great motivating example I’ve seen is an Amount type parametrised by currency as well as the numerical value, so that the type system can enforce that you don’t add two amounts of different currencies, or that to add, you have to also provide a correctly typed exchange rate value.

bgirard 8y ago

I suggested a similar trick in Gecko when we were seeing too many bugs in the rendering/async scrolling code because of mistakes when transforming between the different unit spaces: https://dxr.mozilla.org/mozilla-central/rev/4303d49c53931385892231969e40048f096b4d4c/layout/base/Units.h#385-465 https://dxr.mozilla.org/mozilla-central/rev/4303d49c53931385... Transformations between units are also typed so you wont accidentally use the wrong scale factor when transforming.

Gibbon1 8y ago
Working on porting code with time units that are totally unspecified. Sometimes it's seconds, ms, 1/256th of a second or HH:MM:SS. Just shoot me.
- insulanian 8y ago
  You need F#'s units of measure [1]. [1] https://fsharpforfunandprofit.com/posts/units-of-measure/ https://fsharpforfunandprofit.com/posts/units-of-measure/

dfan 8y ago

I have a system set up in C++ to make it trivial to add new unique kinds of IDs (wrappers around ints) as well as vectors that can be indexed only with that kind of ID. So you can have a ShoeVec containing Shoes that is indexable only by ShoeIDs and a ShirtVec containing Shirts that is indexable only by ShirtIDs. It's zero-overhead in optimized builds, of course. You'd be surprised how rarely you have to convert to or from the underlying type.

jdonaldson 8y ago
Fwiw the Haxe language calls this an "abstract type", and they're very useful. https://haxe.org/manual/types-abstract.html https://haxe.org/manual/types-abstract.html
- deleted 8y ago
  [deleted]
- rurban 8y ago
  Generic types are useful, but still should be called as such, or for the new fad: dependent types. Abstract types would not allow instantiation.
  - jdonaldson 8y ago
    Haxe abstract types are distinct from abstract classes, but I need to learn more about dependent types.
kazinator 8y ago
Congrats, you almost have Pascal there.

jph 8y ago

The article's example boils down to this pseudocode: function foo(s, i) { s * i } s = "hello" i = 2 foo(i, s) // BUG. The runtime crashes. The article advocates adding a type system to detect the bug: function foo(String str, Integer int) { s * i } String s = "hello" Integer i = 2 foo(i, s) // BUG. The compiler detects the error. If you're interested in these kinds of errors, then you may also want to consider ideas such as named parameters: function foo(text: s, count: i) { s * i }

amzans 8y ago
The problem with named parameters is that you can theoretically still pass the wrong value, and in practice not everyone is using named parameters on every function call. By relying on the type system you can catch that issue at compile time and not have to worry about it. We use this technique at work when there’s lots of fields in our data types as it’s nice to be able to keep track of the types during all the transformations and to avoid subtle bugs. Specially as the codebase is constantly changing.
- jph 8y ago
  I agree with you. My opinion is that type checking helps, and so do assertions, borrow checkers, pen testers, etc. The tradeoff IMHO is that these take some time and thought to do well. Would you be willing to send me an example of your best-case for using a type system? For example some code where you feel the type system really helps you and your team? I keep a log of these real world areas, for training my teams. Anonymized code is fine. My email is joel@joelparkerhenderson.com. Thank you!
- tayo42 8y ago
  Do you do this for every string, int, float etc..? Any downsides you run into? I always thought it would be interesting to try it using a type even if it wraps something but never had tried going all in on the idea. In scala do you not use alias ever? I guess they don't help much? Alias of strings can be used interchangeably I think?
  - 8y ago

amzans 8y ago

Something that I enjoy very much in Scala is sealed traits + case classes. sealed trait Food case class FishTaco(size: FishSize) extends Food case class Burger(numPatties: Int) extends Food case class Spaghetti(sauce: PastaSauce) extends Food It’s like Enums + Data Classes on steroids. You can pass around and transform your data as usual, but if you forgot to handle a specific case when doing pattern matching you’ll get a compile warning. For example in the following case: input match { case Burger(patties) => ... case Spaghetti(sauce) => ... } The compiler will happily yell at you something like: warning: match may not be exhaustive. It would fail on the following input: FishTaco(_) Little things such as this one help reasoning about your program since you can rely on the types describing what is possible and what is not.

deleted 8y ago
[deleted]
Rapzid 8y ago
If you like that kinda thing you should check out F# as well. The IDE experience/speed is much better for F# IMHO, but I have a lot of respect for the concepts behind both. And of course they ride on completely separate massive ecosystems, so you can't exactly swap them out willy-nilly.. I wish I could figure out why my IDE experience with Scala and IntelliJ(IDEA) was so darn sluggish. Also hoping they jump on the language server protocol bandwagon in the future.
- brianberns 8y ago
  Yep, these are called "discriminated unions" in F#. I think most functional programming languages have something similar. The underlying concept is "algebraic data types": You can compose types as products (tuples or records) and sums (discriminated unions) of simpler types. From there, you can actually use algebra on types, which is pretty mind-blowing. For example, we can define a generic sum type called Either: Either a b = Left a | Right b You can think of Either as the sum of types "a" and "b": a + b. Tuples are product types, so you can use the distributive property of multiplication over addition to establish that: (a, Either b c) = Either (a, b) (a, c) Or algebraically: a * (b + c) = (a * b) + (a * c) This is one of those areas where category theory is actually useful for programmers.

grosjona 8y ago

The problem with complex type systems is that they force you to spend a lot of your development time thinking about type structures and their relationships (in a universal way) instead of thinking about actual logic (in a more localized way). For example, when you introduce third party modules into your code, sometimes it's impossible to cleanly reconcile the type structures exposed by the module with the type structures within your own system... You may end up with essentially identical concepts being classified as completely different types/classes/interfaces... It creates an unnecessary impedance mismatch between your logic and the logic exposed by third-party modules. This type impedance mismatch may discourage developers from using third-party modules altogether. That might explain why dynamically typed languages like JavaScript and Ruby have such rich third-party module ecosystems compared to that of statically typed languages. Unless there is a single standardized and universally accepted type system which is fully consistent across the minds of all developers of a specific language/platform (for all possible applications), then a type system makes no sense at all; especially a complex one.

whateveracct 8y ago
Those impedance mismatches are equally present in dynamically typed code. The only thing types do is help make it obvious when there are problems with composition. I work in Haskell with many other Haskell developers and a wide variety of Haskell mindsets. It’s a very complex type system we use a lot of, and so far, the issues you mention are so minor and worth it.
- grosjona 8y ago
  With dynamically languages, the type of an object is not important so you don't need to explicitly typecast external objects to fit into your logic. With dynamically typed languages, if two different objects expose the same functions then you can use them in the same way. The behavior of an object is all that counts.
  - wtetzner 8y ago
    You seem to be talking about nominal types being a problem. Structural subtyping and row types are two ways of getting the benefits you're talking about while still being statically typed.

49bc 8y ago

I’m seeing a little bit of a waterbed effect here. The author has replaced the basic type with one that matches it in name. You will never accidentally send CustomerId to CartID because the compiler will fail... but now we’ll nees to dig through the code to find out whether customer ID should be an int, int32, String.... what the heck is it anyway? In scala can I not just say foo(item1=item1) even if foo takes only 1 arg?

tytytytytytytyt 8y ago
> In scala can I not just say foo(item1=item1) even if foo takes only 1 arg? Why would you want to do that? That's less succinct than foo(item1). What are you really asking?
amzans 8y ago
Usually you would lookup the definition of those types just as you do for the function that you are trying to call. At least it’s a good idea to know what a function accepts before passing around your customer IDs ;) And to answer your last question, yes in Scala you can use named parameters like in your example.

lihaoyi 8y ago

I wrote a blog post that goes into a lot more detail into some of these techniques, in case anyone wants to dive deeper - http://www.lihaoyi.com/post/StrategicScalaStylePracticalTypeSafety.html http://www.lihaoyi.com/post/StrategicScalaStylePracticalType... - http://www.lihaoyi.com/post/StrategicScalaStyleDesigningDatatypes.html http://www.lihaoyi.com/post/StrategicScalaStyleDesigningData...

andreygrehov 8y ago

I believe a lot of similar concepts are explained in Domain Driven Design.

GavinMcG 8y ago

This got me thinking, and I'm curious what a language would look like if basic types weren't directly usable. In other words, maybe type checking doesn't go far enough: checking that I'm getting an int is less valuable than checking that I'm getting the right sort of data for the domain.

daxfohl 8y ago
unsigned int?
tzahola 8y ago
See Boost.Units: https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.html https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.h... It enforces correct units/dimensions at compile time, so you won’t be able to mix up length with time or area, etc.
ghayes 8y ago
This might be a good time to check out algebraic data types, esp. with a single constructor. For example, in Elm you might declare: type Length = Inches Int Then any function that accepts a Length, you can only pass in a length. This effectively acts like tagged tuples verified at compile time. You can later extend this type to be: type Length = Inches Int | Meters Int and any code that reads length would have to handle both cases (also checked at compile that). I have found this to be a great way of ensuring all of your types are correct (and sometimes, a great frustration of wishing I didn't have to wrap/unwrap types so often).
- GavinMcG 8y ago
  Yeah, that's one of my favorite takeaways from Elm. I'm thinking of it in an OO style, where perhaps instead of wrapping/unwrapping you're specifying an analog to object properties.
- insulanian 8y ago
  F# has units of measure [1], which are very nice for such a case you're describing. [1] https://fsharpforfunandprofit.com/posts/units-of-measure/ https://fsharpforfunandprofit.com/posts/units-of-measure/

tzahola 8y ago

Even though people love bashing Objective-C for its “weird” method syntax, it trivially circumvents these kind of problems. Also related: Mike Ash’s post about using single-member C structs instead of unitless scalar types: https://www.mikeash.com/pyblog/friday-qa-2013-08-02-type-safe-scalars-with-single-field-structs.html https://www.mikeash.com/pyblog/friday-qa-2013-08-02-type-saf...

platz 8y ago

Make illegeal states unrepresentable

CharlesMerriam2 8y ago

There is often an I love {Scala|Rust|Erland} post showing an simple type issue and claiming that using a bunch of new syntax would somehow fix it. <rant> 1. I want a minimum of typed syntax for safety. For example, remember Hungarian Notation? My linter barfs if I try "icCart = ipMyProduct" because of the semantic type issue. 2. I want a full set of primitives. For example, counts (c) are 0 or above, not infinite, can do arithmetic) while ids (i) are positive, not infinite, cannot do arithmetic, cannot assign constant). I want optionals; I want clearer error handling; I want fully declared I/O instead of manual error handling; I want better. 3. I want tallies of how often simple types are confused before changing languages to fix. My type confusions are complicated nested collections or variant records. </rant> Typing is a means for correct programming, not an end in itself.

jpitz 8y ago
>Typing is a means for correct programming, not an end in itself. That's not always the case. https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview

hardwaresofton 8y ago

If you like this, you're probably also going to like Haskell/OCaml/Ada/F#/Coq (ML family of languages?): I'll leave links for Haskell since the only one of those I've tried and liked personally: https://www.haskell.org/ https://www.haskell.org/ http://learnyouahaskell.com/ http://learnyouahaskell.com/ IMO Haskell is the type system you wanted Java to have, with even more strictness. While it's possible to write unsafe haskell, just about everything you will read, and the language itself encourages you to push as many worries as you can to be solved by the type system. If that doesn't get you excited, there's actually a saying that is mostly true in my experience writing Haskell -- "If it compiles, it works"(tm). Also Haskell on the JVM if you want to dip your toes in: - https://eta-lang.org/ https://eta-lang.org/ - https://github.com/Frege/frege https://github.com/Frege/frege [EDIT] - If you try to learn haskell you'll inevitably run into the M word which rhymes with Gonad. The best guide I've ever read is @ http://adit.io/posts/2013-04-17-functors,_applicatives,_and_monads_in_pictures.html http://adit.io/posts/2013-04-17-functors,_applicatives,_and_... BTW, be ye warned: when you start understanding/getting cozy with the concepts introduced by Haskell you'll wish they were everywhere, and they're not. Languages without proper union types will look dumb to you, easy function composition/points free style will be a daily desire, and monadic composition of a bunch of functions will be frustratingly absent/ugly in other languages, not doing errors-as-values will look ironically error-prone. [EDIT 2] - More relevant to the actual post, how you would do this in Haskell is using the `type` keyword (type aliasing, e.g. `type Email = String`) or the `newtype` keyword, which creates a new type that is basically identical (what the article talks about). Here's some discussion on newtype: - http://degoes.net/articles/newtypes-suck http://degoes.net/articles/newtypes-suck (this article is good, it describes the premise, promise, shortcomings, and workarounds, forgive the clickbaity title) - https://www.reddit.com/r/haskell/comments/4jnwjg/why_use_newtype/ https://www.reddit.com/r/haskell/comments/4jnwjg/why_use_new...

Silhouette 8y ago
Although Haskell has a relatively powerful and useful type system, you are perhaps being a little kind to it here. Haskell also has partial functions, including quite a few dangerous examples in the standard library, various mechanisms to escape the type system entirely, and 27 different ways to handle errors, 28 of which look a bit like exceptions but need handling in 29 different ways. And it still can't handle basic record types very elegantly, nor dependent types such as fixed-size arrays/matrices. Haskell's type system does have a lot going for it and it also makes a useful laboratory for experiments with type-based techniques, but as far as safety goes it has never really lived up to the hype, and for all its advanced magic, it is surprisingly lacking in support for some basic features that are widely available in other languages.

hzhou321 8y ago

The suggested type system adds a lot of code and complexity. For the specific case, I suggest we can try a convention-based solution. Let's, eg. establish a convention that all product id variable named with `prod_` prefix and customer id variable named with `cust_` prefix. Then a simple static analyzer filter can serve as the unit test to catch mistakes (include passing in variable names that don't conform the convention). We should recognize that the enforced prefix serves the same role as the type system but at the preprocessing stage rather than the compiler stage. It does not require the programmer to add any extra code; rather it helps one of the difficult problems of naming things. Unlike the type system, it is easy to adopt strong convention (the strongest being a set of fixed names) and then relax the convention as the program evolves. In contrast, the type system often takes the opposite path of from relax to strict with steep increasing cost. Of course, unlike the type system, the enforcement of the convention does not come automatically -- the programmer has to write static analysis code to enforce it -- this is fundamentally not different from writing unit tests. But the static analysis code is easy to write and less likely to have bugs (and bugs have less severe consequences). I use a general purpose preprocessor, MyDef, and every line of my code goes through several places of filtering anyway, so adding a set of static checks seem trivial. But even you don't use a preprocessor, implementing a simple static convention checker (to be enforced at repository check-in) doesn't seem difficult.

nine_k 8y ago
> unlike the type system, the enforcement of the convention does not come automatically This defeats the whole purpose. > the programmer has to write static analysis code It is legwork that should be relegated to the computer. And, in fact, has been for a long time. I don't only mean type systems; various linters and checkers work where the compiler proper does not (see valgrind or findbugs). Frankly, a lot of test cases for code can be written automatically; the prime example is Haskell's QuickCheck, but a number of other languages has similar tools, all the way down to fully dynamic ones like Python.
- hzhou321 8y ago
  Creating and maintain type system is also leg walk (and I was arguing it is a bigger burden of leg walk). And a Turing complete type system can have Turing complete errors. Let's not pretend we have silver bullet and have a fair discussion

dclowd9901 8y ago

What really put me on to typing JavaScript was this. The ability to avoid unit tests. And frankly what unit test would ever even capture something like this, an implementation issue, (unless you refactored a lib).

clintonb 8y ago
> Don’t get me wrong I’m not saying to scrap all your test suites and try to encode all your constraints using the type system instead. Not at all I still firmly believe that tests are useful but in some cases you can leverage the type system to avoid mistakes. You should still write unit tests. You should also write integration/functional tests that might have caught this error when you tested the code that calls the function in question. The only scenario I can see the argument swapping bug not being caught is when all of the ID arguments equal the same value.

dnomad 8y ago

Types can definitely help with data well-formedness but personally I'm very suspicious of 'mini-types' like Name and CartID. If the data you're wrapping has no internal structure (that can be formally verified) and you're just using the type system as an argument checker then it's not clear to me that you're really adding much value. If CartID and ProductID are both just strings what's to stop a user from doing the same as: CartID cartId = new CartID(productId.toString()); addToCart(..., cartId, ...); <-- but look that's really a ProductID! I'd suggest that while you may have reduced the likelihood of certain errors you have not actually eliminated those errors. The right approach here is to be very suspicious of any methods in your domain that just take a bunch of IDs. Either: (a) Force the caller to resolve the IDs to actual entities before invoking the method: addToCart(Cart c, Product p, ...) or (b) Represent the method parameters as a Parameters object or, preferrably, an Event object. handle(ProductAddedEvent event); The real problem here is not the type system but a domain that is not sufficiently protected by an Anti-Corruption Layer [1]. Unfortunately most developers are not familiar with this kind of strategic design and languages are not much help here. It would be interesting if there was a language that could flag things like weak ACLs. [1] https://docs.microsoft.com/en-us/azure/architecture/patterns/anti-corruption-layer https://docs.microsoft.com/en-us/azure/architecture/patterns...

gcommer 8y ago
> new CartID(productID.toString()); With good data modeling and safety checks, this should fail: a product id and cart id should have some sort of distinguishing syntax (eg "P1234" vs "C1234") and so `new CartID("P1234")` will fail. At some point, no sorts of type system can stop incorrectly implemented/specified logic. An even simpler example would be just passing some constant, valid, but not semantically correct string to the CartID constructor. Your (a) and (b) solutions don't solve this. I could just as easily create a meaningless Cart object, or a meaningless ProductAddedEvent the same way you constructed that meaningless CartID.
- dnomad 8y ago
  As I said, if your data actually has internal structure that can be verified then the Type is meaningful. (Though that sort of prefixing introduces its own problems and I think most IDs just end up being UUIDs or URIs or numbers.) Otherwise you're just wrapping strings. The point here is that a Type represents data and behavior or, more formally, Types represent constraints over a space of data and behavior. Types that don't actually do any constraining are useless. > I could just as easily create a meaningless Cart object, or a meaningless ProductAddedEvent the same way you constructed that meaningless CartID. The problem here is not mixing up IDs. The problem is actually guaranteeing that the pre-conditions of addToCart() have been satisfied. Here, for example, addToCart() probably wants more than just a Cart and Product object, but a Cart and Product objects that have been persisted. Presumably the domain has been constrained so that you can't create meaningless objects. Otherwise what's the point of any object? If the only valid Cart and Product objects are those that can be retrieved from a persistent repository then, yes, this not only solves the trivial problem of mixing up IDs, but also the more valuable underlying problem that addToCart() is constrained to act on real, valid (according to the domain) Cart and Product objects. In other words, this isn't really an issue of language design. And while there's a tendency to believe the language can solve every problems and that design patterns are a sign of language "weakness" the reality is developers that really want to solve these problems will have to think carefully about their domain and apply the appropriate design patterns.

billfruit 8y ago

One thing that I personally would find useful is a F# like Unit of Measure, kind of type metadata, that allows units of quantities to be explicitly mentioned, and there by help in preventing unit confusions in code, ie passing around values in the wrong kind of units, esp degrees and radians for eg, can often be a difficult mistake to catch.

thankthunk 8y ago

Leverage the type system? Type systems exists to allow you catch errors at compile time. That is what it's there to do. It's like saying leveraging the compiler to compile or leveraging the cup to drink water.

rurban 8y ago

The id type parameter is not called phantom type, it's called generic type.