IntroductionCompilers have been used to enforce code safety properties since the beginning of the modern computing era: if your program type-checks, you can be sure that you will not encounter a type error at runtime (modulo any explicit casts you might have inserted yourself). Type-safe languages can reduce the number of program bugs and generally ease the programmer's burden, at the usually mild cost of requiring them to deal with type error messages from the compiler. Security-typed languages are the natural extension of this technology used for program data security. Instead of verifying that your programs are type-safe, these compilers can check that your program is well-behaved from a security standpoint: it does not leak secure data or violate data integrity. There are three security-typed language implementations: Jif and Flow Caml (enforce noninterference), and SELinks (can enforce a variety of security policies, including noninterference). Unfortunately, due to a variety of reasons, security-typed languages are written as their own compilers and generally do not operate on real-world code. Though Jif extends the Java language and Flow Caml extends Caml Special Light, these languages by their nature admit fewer programs than their base compilers, meaning that it is non-trivial to convert a program written in Java into one written in Jif. Security-typed languages need to be able to operate on legacy code if real-world systems are to be built and given stronger security guarantees. My research explores what kind of tools we need to help programmers convert their programs to a security-typed equivalent program, and explores how we can automate this process. |