Colloquium Details
Secure Computing Through Types
| Author: | Bratin Saha Yale University |
|---|---|
| Date: | February 21, 2002 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
The security of computing systems has become crucial with the increasing dependence of businesses and society on networked information systems. In my research, I have been exploring how techniques from modern language technology can be used for constructing secure computing systems.
In this talk, I will show why I believe that language technology offers a more robust solution. In particular, I will concentrate on certifying compilation. A certifying compiler generates not only the code, but also a proof that the code follows a safety policy. I will talk about the challenges in certifying compilation, and how expressive type systems can be used to solve those challenges.
I will discuss the design and implementation of one such type system. The system is powerful enough to type-check services like a garbage collector. It also allows the explicit representation of proofs and propositions. I have implemented the system in a version of the Standard ML of New Jersey compiler. I will discuss the implementation and show the performance on some benchmarks.
Biography
Bratin Saha is a Ph.D. candidate in the Department of Computer Science at Yale University. He received his M.S. in Computer Science from Yale University and his B.Tech. in Computer Science and Engineering from Indian Institute of Technology, Kharagpur. His main research interests include design and implementation of programming languages, compilers, type theory typed intermediate languages, proof carrying code, security and formal methods.