[cap-talk] David Wagner's Google techtalk is now up!

[Jonathan S. Shapiro]

On Thu, 2007-12-13 at 19:22 +0100, Valerio Bellizzomi wrote:
> On 13/12/2007, at 0.15, Mathieu Suen wrote:
> >But can you tell me which security bugs that a static type language  
> >can prevent that dynamicaly type system can't?
> 
> Most of the bugs that are hidden behind control-flow gaps.

I am about to ramble for a moment, and what follows may be utter crap,
but here it goes.

Modern, statically typed, safe programming languages universally include
dynamic typing in a limited way. The problem is unions, and the need to
ensure that the union tag field has been properly checked when code
operates on that union leg. ML, Haskell, BitC, and so forth all perform
checks of this sort.

What is striking (to me) about these checks is that (1) these are
dynamic type checks, but (2) their safe use is enforced through
syntactic means.

Observation: any dynamic type check that returns "true" implicitly
defines an execution scope within which the *static* type of the checked
item is fully known. Matters may become complicated if the language
supports aliasing and mutation (as in BitC), but the principle still
holds.

This prompts me to wonder whether a similar syntactic support mechanism
might not be contrived for more dynamic languages.


Finally, a side comment on the whole static/dynamic issue. There are
real restrictions that a safe static type system imposes. One, which
MarkM can explain better than I, is that static types and first-class
messages are not really compatible (more precisely: first class reply
messages) within the current state of the art of type theory.

In practice, however, I have not found any of these limitations to be
compelling practical problems. This leads me to the opinion that the
static/dynamic "battle" is *usually* a battle about something else
entirely: the cost of annotating a program with types. And it is less
about the cost of annotation per se than it is about the cost of being
required to annotate before appropriate types are properly known (e.g.
in early prototyping). Once they get over the new user hump, ML and
Haskell users do not seem to incur much prototyping overhead in
comparison to users of more dynamically typed languages.

The first class message issue is arguably quite real, but it occurs at
exactly the place where the runtime meets the language, and I/O is
inherently a place where static typing breaks down at the boundary in
all languages.

shap