Streaming media content providers face a variety of adversaries. At the large scale at which they operate, they can justify defense in breadth: different techniques against different adversaries. Existing analysis techniques awkwardly handle questions about a distribution of adversaries against an evolving series of protocols. Contemporary streaming-media protocols eschew full-stream DRM in favor of token-based authentication at the start of each connection. Very recent protocols from several vendors package content in chunks of a few seconds each, rather than a stream continuing for an entire film or live event. Practical attackers work by copy and paste of these authentication tokens, sharing URLs to pay-per-view content in chat rooms or web forums. Others use ``deep links'' to chunks or lists of chunks to view freely available media in ways that violate the wishes of the providers. Accidental behaviors of so-called transparent proxies similarly violate the goals of the providers. We formalize these attacker descriptions in terms of an adversary who can only comprehend some tags in a tagged-concatenation Strand Spaces model. We use this model to show how current streaming protections work and fail, and suggest directions for new streaming media protocols.
MITRE Tech Report 2007 (PDF)
The design of a trusted system based on the Trusted Computing Group's Trusted Platform Module (TPM) was analyzed to understand the role and trust relationships of the TPM, firmware, and software modules involved. The objective was to confirm that the measurements stored and reported by the TPM can successfully discriminate a normal boot sequence, which leaves trusted system software in control, from an insecure one, where some trusted modules might have been replaced by malicious ones. The principal tool used in the analysis was the SMV symbolic model checker.
MITRE Tech Report 2007 (PDF)
Attestation is the activity of making a claim about properties of a target by supplying evidence to an appraiser. An open-ended framework for attestation is desirable for safe support to sensitive or highvalue activities on heterogeneous networks.
We identify five central principles to guide development of attestation systems. We argue that (i) attestation must be able to deliver temporally fresh evidence; (ii) comprehensive information about the target should be accessible; (iii) the target, or its owner, should be able to constrain disclosure of information about the target; (iv) attestation claims should have explicit semantics to allow decisions to depend on several claims; and (v) the underlying attestation mechanism must be trustworthy.
We propose an architecture for attestation that is guided by these principles, as well as an implementation that adheres to this architecture. Virtualized platforms, which are increasingly well supported on stock hardware, provide a natural basis for our attestation architecture.
MITRE Tech Report 2006 (PDF)
A compositional approach to protocol design and analysis is recognized as advantageous. We wish to perform design decomposition in a way that permits independent design and verification of components, and preserves security and correctness goals when the components are recombined. There are many different ways in which composition can be interpreted and implemented. Our version of composition applies to the design of secure protocols. Our objective is to extend verification techniques based on abstract encryption models to protocols that incorporate or implement encapsulated services.
MITRE Tech Report 2006 (PDF)
MITRE has developed Polgen, a tool for human-guided semi-automated policy generation. We initially designed Polgen for use by security administrators confronting unfamiliar programs and obliged to integrate them into existing policy. However, SE Linux adoption will come about when application authors can also at least bootstrap the policy generation process. Polgen works by processing traces of the dynamic behavior of a target program. By observing information flow patterns such as Pipeline, Interpreter, or Proxy in that behavior, Polgen creates new types when appropriate and generates policy based on the patterns it has detected. Because the dynamic behavior is insufficient to fully inform security policy, Polgen presents a wizard-style interface for human interaction. We call the interaction “guided automatic policy generation.” This paper highlights the needs for type generation support, Polgen's pattern recognition capability, and our future plans for human-guided automation. The primary challenges are the introduction of new types, and the use of the M4 macro language as the primary vehicle for abstraction.
Trust in Global Computing 2005 (postproceedings, LNCS 3705) (PDF)
A programming language for cryptographic protocols eases design and implementation of application-specific protocols for tasks such as electronic commerce and distributed access control. The language provides and minimal expressiveness useful for defining new protocols. We give the language a semantics via strand spaces, so that the designer can prove that a new protocol meets the security goals. This semantics also motivates a compilation strategy, yielding protocol implementations faithful to their verified behavior.
We also aim to clarify the relation between the abstract models used in protocol verification and the actual behavior of protocols as implemented.
European Symposium on Programming 2004 (PDF)
Baccalaureate Thesis, Massachusetts Institute of Technology, 2000 (PDF)
The Free Haven Project is a distributed anonymous data haven: a way of anonymously storing and retrieving files. It's designed to encourage free speech in places where that's currently difficult, and to remove the repercussions for being associated with unpopular ideas. The messaging component of Freehaven evolved into the Tor anonymizing overlay network.
This is a demonstration of how easy it is to write software for Linux, X11, and Gnome using the Glade interface generator, and then to package it for Debian. I'd written a moderate amount of software before, but had not worked with any of these environments; this program took me about two hours from conception to final packaging. Most of that was fiddling with interface possibilities. It happens that Dieroller is a useful demo: some friends and I use it when playing games which otherwise require rolling buckets of dice.
Coins is a Palm Pilot application to flip a bunch of coins in a row, until it gets a certain number of heads. This is a common mechanic in some LARPs, and I always seem to drop the coins and have them skid off into corners. It's much nicer to hit a few buttons and go back to talking to people while the program clicks away.
A simple tool to generate random treasure for monsters in a D3D game. The treasure table is not complete, but I welcome additions and will add them to the tool. Requires Python to run.
This is a collection of perl and postscript code to generate pretty wall-poster schedules. I picked it up from somebody at MIT and modified it further; I think the color code came from Richard Tibbetts. It's of limited usefulness for somebody whose schedule isn't as fixed as most college students.
zchosen, zr and zrandom are Perl scripts which select a short phrase from a flat database for use as a signature. They're not useful in their current forms outside of the MIT Zephyr environment, but zchosen in particular has some neat ideas which could easily be adapted to e-mail signatures: it looks at the text of your message, and tries to pick the most relevant signature, based on words in common which are otherwise rare. Zchosen was originally written by Roger Dingledine, and zr and zrandom are based on dozens of examples — these might be cribbed from zsig randomizers by Jay Muchnij and Joe Foley, but I'm no longer certain.
These are the configuration files for my setup of Zsh, Emacs, Gnus, X11, and Ratpoison (an X11 Windowmanager).
The human mind is meant to solve problems. That's how we learn and grow. Games are fun: our brains reward us for training. Easy games are less fun. Hard games are more fun. Narrow games are less fun. Broad games, encompassing many skills, are more fun. Games which develop tactics, resource allocation, creativity, and public speaking are no longer uncommon. The glass-bead game is not yet written, but here follow notes and resources for some of my favorites.
The glass-bead game does not yet exist, but the sprawling, weeks-long games of the MIT Assassins' Guild are one approximation. I have contributed to five:
Summer 2003, with Kat Allen and Andy Menard
That is not a misspelling. This is a game in the tradition of the Guild's "Antartic Base" games, focusing on teams of Space Marines sent to pacify and reconstruct a Vespid world.
Five runs, Spring–Fall 2000, with Ariel Segall and Charles "Ricky" Leiserson, Jr.
Hive is a one-night game for about twenty players set in the Tattoine cantina made famous in George Lucas' Star Wars.
January–April 2000, with Ariel Segall
Gathering was meant to run for only a month, with a few dozen players. It eventually continued for 100 days, involving nearly thirty people. We learned a great deal about the embedded narrative structures necessary to push a game to conflict and closure. In other words, it far overran its slot because the characters reached a stable state of simmering cold conflict.
Spring 1997, with Jim Waldrop
Assault was an experiment in the comparative tactics of offense and defense. The run-time experience is the first time I understood the O-O-D-A loop concept.
February 1997, with Debbie Rhoads, Mike "Hex" Moore, Jim "Fnord" Waldrop, Larry "Larry" DeLucas, and Camilla Fox.
Showdown is a ten-day game for 60 persons. A team of six wrote it in two months. This is considered unusual. Running it certainly cost each of us a point or more of GPA, many hours of sleep, and more than a few points of sanity.
Lots of college students play "Killer", "Assassin", or similar. At MIT, those are called "Circles of Death". My own variant rules for Circles are one node of the bushy tree of evolution of such games.