Writer’s Unblock

I’ve recently got a few technical papers out the door involving Haskell, physical-layer protocols, SMT, security modeling, and run-time verification of embedded systems (phew!).  One of the benefits of industrial research is getting your hands involved in a lot of different research projects.

• This paper is about using Haskell to model physical-layer protocols and using QuickCheck to test them.  Physical-layer protocols are used to transmit bits from one clock-domain to another and are used in ethernet, credit card swipers, CD players, and so on.  The gist of the paper is that even though Haskell is pure & lazy, it works great for modeling and testing real-time protocols and even for computing reliability statistics.  I presented it at the Haskell Symposium in September ’09, which was associated with ICFP.  (The talk video is online!)  The paper is a short experience report—indeed, it is the only experience report that was accepted at the symposium.  The Haskell Symposium was an entertaining and friendly environment for presenting.

• This paper actually precedes the Haskell paper, but it extends the results by describing how to formally verify physical-layer protocols using SMT solvers and k-induction (we use SRI’s SAL tool in this work).  The paper is a journal article accepted at Formal Aspects of Computing.  You’ll find at least two things interesting about this article: (1) For all the excitement about SMT, there don’t seem to be a lot of great examples demonstrating its efficacy—the problems described in this paper were (laboriously!) verified using theorem-provers by others previously, and our approach using SMT is much more automated.  (2) We provide a nice general model of cross clock-domain circuits and particularly metastability.

  So if you can verify physical-layer protocols, why model them in Haskell and QuickCheck them (as we did above)?  There are at least two reasons.  First, if you’re using SMT, then your timing constraints need to be linear inequalities to be decidable.  For systems that with nonlinear constraints, QuickCheck might be your only recourse.  Second, QuickCheck gives you concrete counterexamples and test-cases that you can use to test implementations (SMT solvers often return symbolic counterexamples).

• This paper describes a simple model for analyzing information flow in a system (where a “system” could be a program, a network, an OS, etc.).  The main portion of the paper describes heuristics based on graph algorithms for deciding what sort of information flow policies you might want to enforce in your system.  In general, there’s been a lot of work on analyzing access control policies but not so much work in figuring out what kind of policy you should have in the first place (if you know of such work, please tell me!).  The paper isn’t deep, and it’s also preliminary insofar as I don’t describe building a complex system using the techniques.  Still, there’s a small (Haskell) script available that implements the algorithms described; I’d love to see these analyses find their way into a tool to help system designers build secure systems.

• Finally, this report describes the field of run-time monitoring (or run-time verification) as it applies to safety-critical real-time embedded software.  Run-time monitoring compliments formal verification since when a system is too complicated to verify a priori, it can be monitored at run-time to ensure it conforms to its specification.  Not a lot of work has been done on monitoring software that’s hard real-time, distributed, or fault-tolerant—which ironically could benefit the most from run-time monitoring.  The report should serve as a nice, gentle introduction.  The report should be published soon as a NASA Contractor Report—the work was done under a NASA-sponsored project for which I’m the PI.

Don’t hesitate to give me feedback on any of these papers.  Ok, time to fill up the queue again…