[Haskell] Announce: Bytecode Verification for Haskell

[Robert Dockins]

Fellow Haskellers,

I am very pleased to announce that I recently completed the degree 
requirements for my master's.  As a part of those requirements, I undertook 
research that may be of interest to those of you subscribed to this list.  My 
research involved designing and implementing a type verification algorithm 
for Yhc Haskell bytecode.

The final report detailing this research may found at the Tufts CS Department 
technical reports page [1]. The abstract for the report follows this message.  
In addition to the report, I have made available the source code for my 
proof-of-concept implementation, which consists of a simple bytecode compiler 
and verifier.  The source code may be found at the project page for this 
research [2].

If you have questions or comments please either email me directly or take 
discussion to the haskell-cafe or yhc mailing lists.

Thanks,
Rob Dockins


[1] http://www.cs.tufts.edu/tr/techreps/TR-2007-2
[2] http://www.eecs.tufts.edu/~rdocki01/masters.html




Abstract:

In this paper we present a method for verifying Yhc bytecode, an intermediate 
form of Haskell suitable for mobile code applications. We examine the issues 
involved with verifying Yhc bytecode programs and we present a 
proof-of-concept bytecode compiler and verifier.

Verification is a static analysis which ensures that a bytecode program is 
type-safe. The ability to check type-safety is important for mobile code 
situations where untrusted code may be executed. Type-safety subsumes the 
critical memory-safety property and excludes important classes of exploitable 
bugs, such as buffer overflows. Haskell's rich type system also allows 
programmers to build effective, static security policies and enforce them 
using the type checker. Verification allows us to be confident the 
constraints of our security policy are enforced.