gregory m. malecha

Certified Imperative Programs

I am currently working on Ynot, a project hat seeks to make dependent types practical in programming. Ynot is currently developed in Coq using separation logic to handle pointers and effects.

Graphical Programming Languages

The Uccello project (previously known as PreVIEW) was started by Prof. Walid Taha (Rice University) and Stephan Ellner (now at Google) and aims to better connect textual and graphical programming languages including multi-stage programming constructs. Ellner formalized the connection between the graphical and textual representation in his master's thesis which develops a normal form which is 1-to-1 with the graphical representation (every subterm is named in the normal form) and gives a function for term normalization.

My work on the project taught me a lot about languages since this was the first research that I did during undergraduate. My early work was mostly implementation based; writing OCaml for the various transformations and developing an IDE to automatically visualize the graphical representation.

I extended the language several times to make it easier to develop programs in, for example FFT and the classic exponentiation. Deriving sensible layouts automatically is not easy, and even "professional" tools sometimes generate clunky visualizations. I built two layout styles, one which I developed on my own, and one based on several papers.

Hardware Description Languages

Large circuits often exhibit repeating patterns, for example, multi-bit adders can be created by connecting several single-bit adders. Despite the existance of language constructs to facilitate expressing these patterns, many developers are wary of using them since there is no way to check before synthesis whether a design is synthesizable.

To address this problem, I worked with several other members of the RAP group (Cherif Salama, Angela Zhu, and Walid Taha) on a subset of Verilog developed by Jennifer Gillenwater. We formalized it as a multi-stage language and developed a type system to guarantee synthesizability of programs.

Web Security

Despite the prevalence of the internet in modern life, browsers still have many problems which threaten privacy and integrity. To combat this problem, browsers have developed security mechanisms to protect the user from XSS attacks as well as elevation of privilidge attacks.

I worked with Blake Kaplan (now at Mozilla) on the security model in Firefox 2.5. Together, we embedded security checks directly into the JavaScript interpreter so that access checks are guaranteeed to be performed on all potentially bad code. Our patch fixed several open security bugs at the sacrifice of speed. We then investigated the ability to statically optimize security checks and to dynamically cache the results of security checks.

While the dynamic nature of JavaScript makes sound optimization extremely difficult, caching checks improved the performanace over the unoptimized code. The new security model behind JavaScript in Firefox 3 scraps the old model entirely and uses wrappers to control information flow. It would be interesting to better understand the implications of the new system.