[Prev][Next][Index][Thread]

Re: failures

Another example, with a somewhat similar flavor, is the combination
of subroutines and object initialization in the Java bytecode language.
Both subroutines and object initialization are delicate even in isolation.
Freund and Mitchell found that the Java bytecode verifier (in Sun's
JDK 1.1.4) did not treat their interactions correctly. More specifically,
exploiting some loopholes related to subroutines, one could use an
object before its initialization, contradicting the intended properties
of the verifier.

There might be a third example in the work of Gordon and Syme
on typing the intermediate language in Microsoft's Common Language
Runtime. Their paper says "The process of writing this specification,
deploying the executable specification as a test oracle, and
applying theorem proving techniques, helped us identify several
security critical bugs during development." I don't remember seeing
published details of those bugs.

Martin


Matthias Felleisen wrote:

> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> Okay, this didn't work out. Let's try again. 
> 
> Are examples out there that show how naive reasoning about languages
> (not individual programs) is a major problem? 
> 
>   The canonical example is to combine polymorphic let without
>   restrictions with naive generalizations for references, exceptions,
>   continuations, and channels.
> 
> For what else have we needed *any* form of semantics to dispute naive
> generalizations? 
> 
> I for one would find it really neat if we had such a list of examples
> on-line for use in courses at all levels and program officers at
> funding agencies, too.
> 
> Any other examples than the one above? One is a random hit, two is 
> a coincidence, three makes a pattern. -- Matthias
> 
>