[langsec-discuss] Enforcing validation layer with types
will.sargent at gmail.com
Thu Jan 3 22:43:40 UTC 2013
On Jan 3, 2013, at 1:11 PM, "Michael E. Locasto" <locasto at ucalgary.ca> wrote:
> Some thoughts of varying relevancy that this thread sparked:
> I agree it would be nice for APIs to more strongly express their
> expectations about parameter use. Web is a delightful domain for
> examples b/c services and protocols get mashed up together in the name
> of innovation and interoperability. Of course this servlet can send
> email through your cloud service that triggers an SMS to a message queue
> to tweet your coffee pot to start! Securely.
It's not about an expectation of parameter usage; more like exploiting Scala's type system for Design By Contract purposes.
> (A useful tangent here is Fred Schneider's probabilistic type checking
> line of thought.)
I don't understand what you mean.
> I have little operational experience of Haskell or similar languages, so
> I'm happy to be corrected on what follows. But it seems to me that
> strong typing goes only so far...the compiler and the runtime will
> repeatedly enforce certain simple type constraints on your variables,
> but in considering the high-level logic of your program, couldn't the
> code could actually treat different instances of the same type in
> different ways? The sequence and set of functions I apply to an instance
> could be different than I apply to another. This is certainly easy in
> procedural languages. I suggest this leaves room for discerning between
> the "operational" type of different instances. Or maybe this is the
> heaven we're seeking...the opportunity for exploit only exists in logic
> errors, not low-level memory manipulation.
You don't have to use value classes, it's just a nice default. If you're planning high level logic, then you'd probably want to use trait composition to reflect different instances of the same object i.e. an instance of Email have ValidatedAsExistingDomain trait attached to it. Then if you have methods that only take valid emails, they take ValidatedAsExistingDomain as a parameter rather than Email.
> If distimming doshes (wiki "Gostak") has taught me anything, it's that
> one should think about types as an arbitrary composition of actions on
> particular pieces of memory. The collection of actions defines the type.
> The type label only partially constrains eligible actions.
It's not the case that the type is a label that partially constraints eligible actions. Types are a way of constructing proofs to the compiler. For example, you can specify a game of Tic Tac Toe at compile time using the type system:
> In other words, the effective type of a variable instance is what your
> program actually does to the data -- not a label (and the small set of
> simple rules it implies) stated at declaration time in the source. And
> now you are in the pickle of relying partially on the type system to
> enforce some constraints and then partially on yourself or an external
> component to enforce some higher-level constraints...is that composition
> of functionality always predictable and correct?
If you want to enforce higher level constraints using something other than the type system, that's a valid approach as well, and it may be more practical when you have business rules that encompass relationships between several different objects. Nothing is ever guaranteed to be always predictable and correct.
More information about the langsec-discuss