[Haskell] Announce: Bytecode Verification for Haskell
robdockins at fastmail.fm
Mon Feb 12 23:37:02 EST 2007
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 . 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
If you have questions or comments please either email me directly or take
discussion to the haskell-cafe or yhc mailing lists.
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.
More information about the Haskell