[langsec-discuss] Enforcing validation layer with types
Michael E. Locasto
locasto at ucalgary.ca
Thu Jan 3 21:11:16 UTC 2013
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.
(A useful tangent here is Fred Schneider's probabilistic type checking
line of thought.)
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.
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.
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?
Is x an integer...or is it a jump table? Is that a packet structure or a
sequence of function pointers? etc. It depends on what the code does (or
could be made to do) to that memory range. What are the relationships
between a memory range and all the instructions capable of manipulating
it? How do you enumerate & control these relationships? FP languages may
take a big chunk of that worry away, but a principled design of
something that does sound & complete constraint enforcement over an API
or interface is still a challenge, IMHO.
On 12/21/12 2:54 PM, Will Sargent wrote:
> On Mon, Dec 17, 2012 at 10:18 PM, munin <munin at mimisbrunnr.net>
>> I found FP after doing systems programming for many years. This
>> semester I went back into doing a lot of C systems programming and
>> greatly missed the type system of a strong, statically typed
>> functional language!
>> I don't do any web programming or untrusted input processing in
>> ocaml, but it seems like you could naturally express a thought like
>> this by having a separate type for any input data, and then a
>> separate type for any trusted function input. The type system
>> wouldn't let you directly source data through, so you would
>> essentially have:
> It looks similar, but in practice UntrustedInput is going to be the
> "blind type" that's given to you by the framework, so you only
> really need the validated types yourself.
>> a lot of ocaml apis avoid the "blind string" and "blind int" and
>> the language seems to make it easy to provide rich semantic meaning
>> to types. I don't do any web programming though …
> It's funny how much of this is old hat to Haskell programmers.
> There's one guy who said the list read like a "design intro to
> Haskell programming"...
> Frankly I think a bunch of web programming is overblown -- a good
> web framework should be able to render web pages, handle cookies,
> collect form information, and be able to do longpoll / websocket
> streaming for you. Everything else (ORM, Email, etc.) should be
> encapsulated and passed through an API to something that doesn't care
> where it came from. TL;DR -- anything called a web framework should
> only be dealing with DTOs and transient data.
> Will. _______________________________________________ langsec-discuss
> mailing list langsec-discuss at mail.langsec.org
More information about the langsec-discuss