Minx: Simple and Efficient Anonymous Packet Format

Ben Laurie and George Danezis have published Minx, a packet format for anonymous network applications:

http://www.apache-ssl.org/minx.pdf

"Most importantly Minx resists active
attackers that are prepared to modify messages in order to
embed tags which they will try to detect elsewhere in the
network. The proposed scheme imposes a low communication
and computational overhead, and only combines well
understood cryptographic primitives."

Formal Methods

I've been skimming over some papers on formal analysis and robust software. It started with a brow beating from Dijkstra that I ran across. He says some pretty amusing stuff which hits pretty close to home, such as "testing by random sampling is hopelessly inadequate as well, because even the most vigorous exercising possible will only cover a truly negligible fraction of the possible number of cases, and whole classes of in some sense critical cases can --and will!-- be missed: only the most obvious blunders will show up." Thats pretty much what I do for a living!

So 36 years later what are we doing about it? Turns out there are some people working on interesting things.

I've already mentioned the QuickCheck project earlier, which lets you do fuzz testing on small units of code to get better coverage. You specify properties in a declarative fashion and it uses random inputs to verify the declarations. Even better, there's Extended Static Checking for Haskell which lets you specify pre- and post- conditions and uses static analysis to prove that the declarations hold. This augments the strong static checking (which can catch a lot of bugs in its own right) with user-specified properties that can also be verified statically to prevent runtime errors from occuring.

There are two operating system projects which are using formal methods to attempt to build a high-assurance operating system to provide a solid foundation for other programs. The first, seL4 is an L4 variant. This paper talks about how they wrote a formal specification in Haskell (this formal spec is executable!), translated it into the Isabelle theorem prover to verify properties formally and eventually will translate the result into a real implementation in C.

The coyotos project is building a microkernel using formal methods. They're using a new scheme-like language called BitC that has formally specified semantics and has the nifty property that a useable subset of the language doesn't require dynamic allocation (and hence doesn't need garbage collection -- this is cool because you can use it for low-level code without having to piggyback on a large GC implemented in C).

Wouldn't it be cool if people wrote high-assurance versions of security-sensitive software that we need to use every day? Things like SSL, ssh and httpd? Here's one project that's writing some of these in OCaml, a functional programming language with a strong type system. Definitely a step in the right direction.

Automatic Specification-Based Testing

What if all you had to do to test your software was write a few predicates. What if there was a program that would take those predicates and fuzz your program to see if they held up? That's the idea of QuickCheck:
http://www.cs.chalmers.se/~rjmh/QuickCheck/
This works particularly well for functional code where the outputs rely solely on the inputs, but the authors also look into fuzzing stateful code as well.

Engler is a Rockstar

If Dawson Engler was a rockstar, the reviews for his latest album would be great. Check out recent talks on automated generation of test workloads and experiences commercializing his academic work:
http://www.stanford.edu/~engler/exe.ppt
http://www.stanford.edu/~engler/spin05-coverity.ppt
And while you're at it, check out the rest of his page, because if you haven't heard his old stuff yet, well, you should:
http://www.stanford.edu/~engler/

Behavioral Classification

Arr said to add this:
http://www.microsoft.com/downloads/details.aspx?FamilyID=7b5d8cc8-b336-4091-abb5-2cc500a6c41a&DisplayLang=en

Languages Homework

Please read all these papers. There will be a test on friday.
http://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml

A large collection of "great" programming languages papers.

Risk Aversion v. Deal or No Deal

This paper uses the game show Deal or No Deal to measure how people react to risk. The first half is an easy read before it gets very technical.
http://papers.ssrn.com/sol3/papers.cfm?abstract_id=636508

Is Stock Picking Declining Around the World?

Found this via the Economist. Basically, it suggests that the easiest explanation for the growth in "passive investing" (which basically lets the market determine how much you should own of a stock base on it's market cap) is through ... actively traded funds. So much for active management of those funds!

We do three things in this paper. We first develop a metric to measure the maximum fraction of volume explained by stock picking in a market. We then use our metric to measure stock picking around the world. We find that though there is more stock picking in emerging markets than in developed countries, it is declining everywhere. In the United States, for example, stock picking has secularly declined from a high of 60% in the 1960s to a low of 24% in the 2000s. Finally, as markets cannot be efficient if everyone believes that they are efficient and, therefore, do no stock picking - the Grossman and Stiglitz (1980) paradox - we ask what is the long-run steady state fraction of stock pickers? We develop a simple theoretical model, and calibrate this model to the United States economy to conclude that stock picking will eventually settle at 11% of trading volume in the United States.

Source: Is Stock Picking Declining Around the World?, UTPAL BHATTACHARYA, NEAL GALPIN.

While this blog is devoted to technology, this is a tangent that I think many of us entertain, simply because it's so complex and enticing. For myself, I tend to look at it (the behavior of markets) with the same fascination that I bring to thermodynamics, namely "cool, watch it go!"

An Introduction to Applicable Game Theory (Gibbons)

This came across on a mailing list for a reading group I have attended (but fail to attend regularily). This is this week's big read.

This paper offers an introduction to game theory for applied economists. I try to give simple definitions and intuitive examples of the basic kinds of games and their solution concepts. There are four kinds of games: static or dynamic, and complete or incomplete information. ( Complete information means there is no private information.) The corresponding solution concepts are: Nash equilibrium in static games of complete information; backwards induction (or subgame-perfect Nash equilibrium) in dynamic games of complete information; Bayesian Nash equilibrium in static games with incomplete information; and perfect Bayesian (or sequential) equilibrium in dynamic games with incomplete information. The main theme of the paper is that these solution concepts are closely linked. As we consider progressively richer games, we progressively strengthen the solution concept, to rule out implausible equilibria in the richer games that would survive if we applied solution concepts available for simpler games. In each case, the stronger solution concept differs from the weaker concept only for the richer games, not for the simpler games.

Source: Robert Gibbons, 1997. "An Introduction to Applicable Game Theory," NBER Technical Working Papers 0199, National Bureau of Economic Research, Inc.

Game theory is a big interest to a lot of people, mainly because they know it's powerful and complicated. However, I think that introductions like Gibbons' are useful for getting this across to a lot of smart people. Follow the citations of this paper and you'll get a wonderful tour of modern applied game theory.