Edward Z. Yang
I am a second year PhD student at Stanford advised by David Mazières
and John Mitchell. I am a proud member
of the Secure Computer Systems group.
I'm interested in applying operating system mechanisms (hardware
isolation, dynamic resource limits) to the design and construction of
programming languages, and vice versa (type systems, formal
verification, information flow control). I'm a big fan of Haskell, a
non-strict purely functional language.
(I use a ThinkPad X61 Tablet. Find me on
or on Strava, Stack Overflow, Wikipedia, Tripit, Reddit, LinkedIn, Mendeley.)
What are my collaborators and I working on?
Abstraction is a fundamental tenet of software engineering, and it is often enforced through mechanisms such as information hiding. For large software projects, such facilities are considered essential; for security abstractions, this enforcement is mandatory. However, real software engineers repeatedly and profitably violate abstraction: languages that are too inflexible to allow such violations often force programmers to resort to solutions that are worse than the disease. What is going on here? We want to find out. Here are some preliminary thoughts.
A method for adding IFC to existing programming languages
Information-flow control is a promising discipline for enforcing the security of systems. Unfortunately, adding IFC often requires invasive changes to the semantics of the host language. We're working on a general method for adding coarse-grained IFC to a language, while requiring only minimal changes to our semantics. Inspired by Matthews' and Findler's
work on multi-language semantics, our approach is to take a minimal IFC calculus and combine it with the target language to achieve an IFC-enabled language. We hope to validate this approach by showing that the noninterference proof is parametric in the source of language, and that the resulting semantics accurately describe existing IFC systems. Here is a preprint on the topic
The runtime system of a lazy, purely functional language
GHC's runtime system is a complicated beast, its many lines of code spanning many different concerns. How does parallelism and concurrency work? How does the garbage collector work? How is lazy evaluation implemented? These are questions whose answers are scattered throughout the various literature that has come out of the GHC project over the years. We're working on a journal paper which ties all of this literature together, with the hopes that it will be useful for other designers of runtime systems for functional languages (and perhaps non-functional ones too). Here is a draft version of the paper
- Edward Z. Yang, David Mazières. Dynamic Space Limits for Haskell. In Proceedings of the 35th annual ACM SIGPLAN conference on Programming Language Design and Implementation. June 2014.
[ paper | bibtex | reviews/rebuttal (aec, icfp13/rebuttal) | slides ]
- Deian Stefan, Pablo Buiras, Edward Z. Yang, Amit Levy, David Terei, Alejandro Russo and David Mazières. Eliminating Cache-Based Timing Attacks with Instruction-Based Scheduling. In Proceedings of the 18th European Symposium on Research in Computer Security (ESORICS 2013). September 2013.
[ paper (ext) | bibtex | reviews (csf13, oakland13) ]
- Erik D. Demaine, Pavel Panchekha, David Wilson, Edward Z. Yang. Blame Trees. In Proceedings of the 12th International Symposium on Algorithms and Data Structures (WADS 2013). August 2013.
[ draft | bibtex | reviews | slides | video ]
- Edward Z. Yang, Deian Stefan, John Mitchell, David Mazières, Petr Marchenko, Brad Karp. Toward Principled Browser Security. In Proceedings of The 14th Workshop on Hot Topics in Operating Systems (HotOS XIV), USENIX 2013. May 2013.
[ paper | bibtex | reviews ]
- Edward Z. Yang. Academic software reuse, an experience report. 6.UAP report advised by Adam Chlipala. May 2012.
[ paper | bibtex ]
What do I do in my free time?
Some projects I'm associated with...
of the News
|a visual metaphor for interconnected story lines|
||an interactive GHC heap profile pastebin|
||an interactive textbook for teaching the sequent calculus|
||a compiler for the functional language Haskell|
||a standards compliant HTML filter|
||a distributed autoinstall management system|
||automatic protection against Cross-Site Request Forgery|
||a magazine about all things Haskell|