A Fistful of Dollars
Posted: March 7, 2012 Filed under: Uncategorized | Tags: big ideas, DARPA, research Leave a comment »A while back I attended an excellent DARPA Proposers’ Day. It got me thinking, “If I had a fistful of (a few million) dollars to provide researchers, what sort of program might I start?” Two ideas struck me:
Getting software right, fast
Software is usually developed in a world with incomplete requirements and with users (and attackers) that try to break your assumptions. Furthermore, more often than not, developers themselves (perhaps with a QA team, if they’re lucky) largely decide when they’re “done”—when a version is bug-free enough, secure enough, and meets the specifications to release.
There are a dizzying number of approaches to improving quality: testing (e.g., unit testing, penetration testing, black-box and white-box testing), compiler tools (e.g., type-checking, warnings), formal verification (e.g., model-checking, static analysis, decision procedures), programming methodologies (e.g., pair-programming, extreme programming), etc. The question is, what combinations of approaches provide benefits and by what factor?
A major portion of the challenge would be to fund experiments that are large enough to draw statistical conclusions about different approaches. Teams would get points for finishing faster, but lose points for bugs, security vulnerabilities, unimplemented features, etc. uncovered by a separate “read team”. To make the experience more realistic, I’d have career programmers (not students in an undergrad course) to participate in the experiments. A major portion of the program would be just designing the experiments to ensure statistical conclusions could be drawn from them, but I imagine the results might be enlightening.
A Believe Search Engine
Imagine a “search” engine in which you could search not for facts, but beliefs. For example, I might query the likelihood that someone believes that the Earth revolves around the Sun in Russia in 1600. Or I might ask what the likelihood of someone believing in global warming in Japan in 2012. Or whatever else. The engine would return some probability, perhaps with a confidence interval. I’d imagine being able to query some believe based on geography, time period, religion, nationality, sex, and so forth. Of course this is a hard, hard problem, and would likely involve search as well technology akin to IBM’s Watson. I’d be curious to know if it were feasible at all.
When Formal Systems Kill
Posted: February 18, 2012 Filed under: Formal methods | Tags: Formal methods, philosophy 1 Comment »What happens when a philosophy professor (with a M.S. in Computer Science) and a formal methods engineer (like me) collaborate? The outcome in my case is a paper entitled, “When Formal Systems Kill: Computer Ethics and Formal Methods” (pdf). In the paper, we give an ethical treatment of the use of formal methods. Our goal in the paper is not so much to make definitive claims on the subject but to raise awareness of the issue for further philosophical treatment. The subject has been neglected by ethics philosophers.
Darren (my coauthor) and I had a hard time deciding where to try to publish this. We ended up submitting it to the American Philosophical Association’s (APA) newsletter on Philosophy and Computers, where it was accepted for the Fall 2011 edition. (The APA is the “ACM of Philosophy” within the United States.)
The paper was a number of years in the making, being a side-project for me. I can’t say I agree with everything we wrote, but I hope it serves as a useful starting point for the dialogue between ethics and formal methods.
Who’s Afraid of Software?
Posted: January 19, 2012 Filed under: Software | Tags: fear, risk, Software Leave a comment »Who’s afraid of software? I mean viscerally, stomach-knotting afraid. Afraid like you might be when you come across a snake or a bear, or when you are mugged. Do you obsess about a phishing attack each time you open your email? Do you worry there’s an eavesdropper when you join the open wifi access point in a coffee shop? Do you worry your software will fail in your modern automobile or aircraft?
I listened to a Freakonomics podcast about risk, uncertainty, and beliefs. One point made during the show was that our fears are shaped by evolution—to our ancestors, it made sense to be afraid of threatening animals. In modern life, however, our fears don’t match risks—we’d be much better off being afraid of cheeseburgers, as pointed out in the show. Some people are afraid of modern risks. I know people afraid of cancer, for example.
That got me thinking about fearing software. Software is certainly among the most complex artifacts created by humans. Modern cars contain 100+ million lines of code. Nearly every day there is a story about a large corporation being hacked and of cyber-warfare between nations.
My question is serious—I really do wonder if people are genuinely afraid of software. I work in the area of software assurance, and while I take precautions against viruses, phishing attacks, etc., I don’t particularly worry about software failures, even when my life might depend on it. This is despite issues just last year like this and this in automotive software. I get to see a somewhat how the sausage is made, and in general, we only exercise a small fraction of the state-space of deployed software in validation and in actual usage. There are legitimate risks, but there seems to be very little fear.
Perhaps like a medical doctors stereotypically neglecting their own health, I don’t worry day-to-day about software assurance despite working in the field. But it seems nobody else really fears software, either.
In the podcast, the topic of polarizing claims, like global warming, is discussed. Outside of academic circles, one’s view on the risks of software are not so polarizing—your views on the topic won’t cause your friends or colleagues to disparage you (indeed, if anything, the main risk is likely boring others in discussing the topic!). I wonder just what the “global warming” of software might be in the future.
Copilot featured in Aerospace America
Posted: December 10, 2011 Filed under: Copilot Leave a comment »My Copilot project, sponsored by NASA, was featured in the Aerospace America magazine “Year in Review” edition (December 2011). We recently finished up the project, which focused on solving the problem of failure in complex embedded systems (like flight control systems in commercial aircraft). Our approach was a language called Copilot for runtime monitoring of embedded systems corroborated with experiments on airspeed sensor systems and an autopilot communication link.
Here’s a link to the page from the magazine mentioning us from the author’s page. (The relevant paragraph is in the middle of the right column).
Thanks to Galois and the National Institute of Aerospace where the work was done, the NASA folks we collaborated with, and especially Alwyn Goodloe, Nis Wegmann, Sebastian Niller, and Robin Morisset who worked on the project with me.
Stable Names in Haskell
Posted: November 26, 2011 Filed under: Copilot, Haskell, Software 4 Comments »Stable names in GHC “are a way of performing fast (O(1)), not-quite-exact comparison between objects.” Andy Gill showed how to use them to extract the explicit graph from writing recursive functions in his Data.Reify package (and associated paper). It’s a great idea and very practical for embedded domain-specific languages—we’ve used the idea in Copilot to recover sharing.
However, consider this example, with three tests executed in GHCI.
For a function with type constraints, stable names fails to “realize” that we are pointing to the same object. As a couple of my colleagues pointed out, the cause is the dictionary being passed around causing new closures to be created. Simon Marlow noted that if you compile with -O, the explicit dictionaries get optimized away.
Here are the solutions I have to “fixing” the problem, in the context of a DSL:
- Tell your users that recursive expressions must be monomorphic—only “pure functions” over the expressions of your DSL can be polymorphic.
- Implement a check in your reifier to see how many stable names have been created—if some upper-bound is violated, then the user has created an infinite expression, the expression is extremely large (in which case the user should try to use some sharing mechanism, such as let-expressions inside the language), or we’ve hit a stable-names issue.
- Ensure your DSL programs are always compiled.
- Of course, you can always take another approach, like Template Haskell or not using recursion at the Haskell level; also check out Andy Gill’s paper for other solutions to the observable sharing problem.
I don’t see how to use (deep)seq to fix the problem, at least as it’s presented in the example above, but I’d be keen to know if there are other solutions.
FM@Galois Talks
Posted: November 10, 2011 Filed under: Formal methods Leave a comment »As I posted over on the Galois blog, I recently gave a talk a couple of times on formal methods at Galois over the years (pdf). It’s been fun putting theory into practice!
Making your Ubuntu life better
Posted: June 18, 2011 Filed under: Software 1 Comment »I’ve had a lot of trouble with Ubuntu 11.04 (Natty Narwhal) on a laptop (ThinkPad 420), and I’ve had problems including:
- Not being able to use dual monitors,
- Random logoffs.
I tentatively think I was able to solve them with two easy fixes:
- Turn off Unity. You can do this in the login screen.
- In the Update Manager, under “Settings”, check “Proposed updates”.
With the proposed updates, Unity may be working; try that at your own risk. With that, I have a reasonably stable system.
Meta-Programming and eDSLs
Posted: January 30, 2011 Filed under: Copilot, Haskell, Software, Uncategorized Leave a comment »I’ve been working on a domain-specific language that is embedded in Haskell (an “eDSL”) that essentially takes a set of Haskell stream (infinite list) equations and turns them into a real-time C program implementing the state-machine defined by the streams. It’s called Copilot, and in fact, it’s built on top of another Haskell eDSL called Atom,1 which actually does the heavy lifting in generating the C code.
For example, here’s the Fibonacci sequence in Copilot:
fib = do let f = varW64 "f" f .= [0,1] ++ f + (drop 1 f)
I’ve been writing Copilot libraries recently, and I’ve had the following realization about eDSLs and meta-programming (let me know if someone has had this idea already!). Many languages treat meta-programming as a second-class feature—I’m thinking of macros used by the C preprocessor, for example (it’s probably generous even to call the C preprocessor ‘meta-programming’). One reason why Lisp-like languages were exciting is that the language is a first-class datatype, so meta-programming is on par with programming. In my experience, you don’t think twice about meta-programming in Lisp. (Haskell is more like C in this regard—you do think twice before using Template Haskell.)
So languages generally treat meta-programming as either second-class or first-class. What’s interesting about eDSLs, I think, is that they treat meta-programming as first-class, but programming as second-class! This isn’t surprising, since an eDSL is a first-class datatype, but the language is not first-class—its host language is.
Practically, what this means is that you spend very little time actually writing eDSL programs but rather generating eDSL programs. It is natural to layer eDSLs on top of other eDSLs.
This is just how Copilot came about: I was writing various Atom programs and realized that for my purposes, I just needed a restricted set of behaviors provided by Atom that are naturally represented by stream equations (and make some other tasks, like writing an interpreter, easier).
But as soon as Copilot was written, we2 started writing libraries implementing past-time linear temporal logic (LTL) operators, bounded LTL operators, fault-tolerant voting algorithms, regular expressions, and so on.
You wouldn’t think about combining the intermediate languages of a compiler into the same program. The idea of a language is more fluid, more organic in the context of eDSLs, where now libraries can be quickly written and different levels can be easily combined.
1Tom Hawkins wrote Atom.
2Credit for Copilot also goes to Sebastian Niller, Robin Morisset, Alwyn Goodloe.
New Group: Functional Programming for Embedded Systems
Posted: May 30, 2010 Filed under: Software Leave a comment »Are you interested in how functional programming can be leveraged to make embedded-systems programming easier and more reliable? You are not alone. For example, check out what’s been happening in just the past couple of years.
- Programming the Arduino micro-controller with Atom/Haskell.
- The Atom eDSL language itself.
- The Feldspar language for DSP (embedded in Haskell).
- Writing a DO178B-compliant compiler in Ocaml (presented at ICFP’09).
- … And others.
Now Tom Hawkins (designer of Atom) has started a Google group, fp-embedded, to discuss these issues. Please join and post your projects & questions!
An Apologia for Formal Methods
Posted: March 14, 2010 Filed under: Formal methods, Software | Tags: Formal methods, IEEE Computer 2 Comments »In the January 2010 copy of IEEE Computer, David Parnas published an article, “Really Rethinking ‘Formal Methods’” (sorry, you’ll need an IEEE subscription or purchase the article to access it), with the following abstract:
We must question the assumptions underlying the well-known current formal software development methods to see why they have not been widely adopted and what should be changed.
I found some of the opinions therein to be antiquated, so I wrote a letter to the editor (free content!), which appears in the March 2010 edition. IEEE also published a response from David Parnas, which you can also access at the letter link above.
I’ll refrain from visiting this debate here, but please have a look at the letters, enjoy the controversy, and do not hesitate to leave a comment!
10 to the -9
Posted: January 24, 2010 Filed under: Fault Tolerance, Hardware | Tags: 10^-9, probability, reliability, safety-critical systems 13 Comments », or one-in-a-billion, is the famed number given for the maximum probability of a catastrophic failure, per hour of operation, in life-critical systems like commercial aircraft. The number is part of the folklore of the safety-critical systems literature; where does it come from?
First, it’s worth noting just how small that number is. As pointed out by Driscoll et al. in the paper, Byzantine Fault Tolerance, from Theory to Reality, the probability of winning the U.K. lottery is 1 in 10s of millions, and the probability of being struck by lightening (in the U.S.) is more than a 1,000 times more likely than
So where did come from? A nice explanation comes from a recent paper by John Rushby:
If we consider the example of an airplane type with 100 members, each flying hours per year over an operational life of 33 years, then we have a total exposure of about 107 flight hours. If hazard analysis reveals ten potentially catastrophic failures in each of ten subsystems, then the “budget” for each, if none are expected to occur in the life of the fleet, is a failure probability of about
per hour [1, page 37]. This serves to explain the well-known
requirement, which is stated as follows: “when using quantitative analyses. . . numerical probabilities. . . on the order of
per flight-hour. . . based on a flight of mean duration for the airplane type may be used. . . as aids to engineering judgment. . . to. . . help determine compliance” (with the requirement for extremely improbable failure conditions) [2, paragraph 10.b].
[1] E. Lloyd and W. Tye, Systematic Safety: Safety Assessment of Aircraft Systems. London, England: Civil Aviation Authority, 1982, reprinted 1992.
[2] System Design and Analysis, Federal Aviation Administration, Jun. 21, 1988, advisory Circular 25.1309-1A.
(By the way, it’s worth reading the rest of the paper—it’s the first attempt I know of to formally connect the notions of (software) formal verification and reliability.)
So there a probabilistic argument being made, but let’s spell it out in a little more detail. If there are 10 potential failures in 10 subsystems, then there are potential failures. Thus, there are
possible configurations of failure/non-failure in the subsystems. Only one of these configurations is acceptable—the one in which there are no faults.
If the probability of failure is then the probability of non-failure is
So if the probability of failure for each subsystem is
then the probability of being in the one non-failure configuration is
We want that probability of non-failure to be greater than the required probability of non-failure, given the total number of flight hours. Thus,
which indeed holds:
is around
Can we generalize the inequality? The hint for how to do so is that the number of subsystems () is no more than the overall failure rate divided by the subsystem rate:
This suggests the general form is something like
Subsystem reliability inequality:
where
Let’s prove the inequality holds. Joe Hurd figured out the proof, sketched below (but I take responsibility for any mistakes in it’s presentation). For convenience, we’ll prove the inequality holds specifically when but the proof can be generalized.
First, if the inequality holds immediately. Next, we’ll show that
is monotonically non-decreasing with respect to by showing that the derivative of its logarithm is greater or equal to zero for all
So the derivative of its logarithm is
We show
iff
and since
iff
Let , so the range of
is
Now we show that in the range of , the left-hand side is bounded below by the right-hand side of the inequality.
and
Now taking their derivatives
and
Because in the range of
, our proof holds.
The purpose of this post was to clarify the folklore of ultra-reliable systems. The subsystem reliability inequality presented allows for easy generalization to other reliable systems.
Thanks again for the help, Joe! Read the rest of this entry »
Writer’s Unblock
Posted: September 30, 2009 Filed under: Software, Verification Leave a comment »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…
Finding Boole
Posted: August 10, 2009 Filed under: Hardware, Verification | Tags: model checking, SAL Leave a comment »Here’s a simple challenge-problem for model-checking Boolean functions: Suppose you want to compute some Boolean function , where
represents 0 or more Boolean arguments.
Let ,
,
,
range over 2-ary Boolean functions, (of type
), and suppose that
is a fixed composition of
,
,
,
. (By the way, I’m going to talk about functions, but you can think of these as combinatorial circuits, if you prefer.)
Our question is, “Do there exist instantiations of ,
,
,
such that for all inputs,
?
What is interesting to me is that our question is quantified and of the form, “exists a forall b …”, and it is “higher-order” insofar as we want to find whether there exist satisfying functions. That said, the property is easy to encode as a model-checking problem. Here, I’ll encode it into SRI’s Symbolic Analysis Laboratory (SAL) using its BDD engine. (The SAL file in its entirety is here.)
To code the problem in SAL, we’ll first define for convenience a shorthand for the built-in type, BOOLEAN:
B: TYPE = BOOLEAN;
And we’ll define an enumerated data type representing the 16 possible 2-ary Boolean functions:
B2ARY: TYPE = { False, Nor, NorNot, NotA, AndNot, NotB, Xor, Nand
, And, Eqv, B, NandNot, A, OrNot, Or, True};
Now we need an application function that takes an element f from B2ARY and two Boolean arguments, and depending on f, applies the appropriate 2-ary Boolean function:
app(f: B2ARY, a: B, b: B): B = IF f = False THEN FALSE ELSIF f = Nor THEN NOT (a OR b) ELSIF f = NorNot THEN NOT a AND b ELSIF f = NotA THEN NOT a ELSIF f = AndNot THEN a AND NOT b ELSIF f = NotB THEN NOT b ELSIF f = Xor THEN a XOR b ELSIF f = Nand THEN NOT (a AND b) ELSIF f = And THEN a AND b ELSIF f = Eqv THEN NOT (a XOR b) ELSIF f = B THEN b ELSIF f = NandNot THEN NOT a OR b ELSIF f = A THEN a ELSIF f = OrNot THEN a OR NOT b ELSIF f = Or THEN a OR b ELSE TRUE ENDIF;
Let’s give a concrete definition to f and say that it is the composition of five 2-ary Boolean functions, f0 through f4. In the language of SAL:
f(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B):
[[B2ARY, B2ARY, B2ARY, B2ARY, B2ARY] -> B] =
LAMBDA (f0: B2ARY, f1: B2ARY, f2: B2ARY, f3: B2ARY, f4: B2ARY):
app(f0, app(f1, app(f2, b0,
app(f3, app(f4, b1, b2),
b3)),
b4),
b5);
Now let’s define the spec function that f should implement:
spec(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = (b0 AND b1) OR (b2 AND b3) OR (b4 AND b5);
Now, we’ll define a module m; modules are SAL’s building blocks for defining state machines. However, in our case, we won’t define an actual state machine since we’re only modeling function composition (or combinatorial circuits). The module has variables corresponding the function inputs, function identifiers, and a Boolean stating whether f is equivalent to its specification (we’ll label the classes of variables INPUT, LOCAL, and OUTPUT, to distinguish them, but for our purposes, the distinction doesn’t matter).
m: MODULE =
BEGIN
INPUT b0, b1, b2, b3, b4, b5 : B
LOCAL f0, f1, f2, f3, f4 : B2ARY
OUTPUT equiv : B
DEFINITION
equiv = FORALL (b0: B, b1: B, b2: B, b3: B, b4: B, b5: B):
spec(b0, b1, b2, b3, b4, b5)
= f(b0, b1, b2, b3, b4, b5)(f0, f1, f2, f3, f4);
END;
Notice we’ve universally quantified the free variables in spec and the definition of f.
Finally, all we have to do is state the following theorem:
instance : THEOREM m |- NOT equiv;
Asking whether equiv is false in module m. Issuing
$ sal-smc FindingBoole.sal instance
asks SAL’s BDD-based model-checker to solve theorem instance. In a couple of seconds, SAL says the theorem is proved. So spec can’t be implemented by f, for any instantiation of f0 through f4! OK, what about
spec(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = TRUE;
Issuing
$ sal-smc FindingBoole.sal instance
we get a counterexample this time:
f0 = True f1 = NandNot f2 = NorNot f3 = And f4 = Xor
which is an assignment to the function symbols. Obviously, to compute the constant TRUE, only the outermost function, f0, matters, and as we see, it is defined to be TRUE.
By the way, the purpose of defining the enumerated type B2ARY should be clear now—if we hadn’t, SAL would just return a mess in which the value of each function f0 through f4 is enumerated:
f0(false, false) = true f0(true, false) = true f0(false, true) = true f0(true, true) = true f1(false, false) = true f1(true, false) = true f1(false, true) = false f1(true, true) = true f2(false, false) = false f2(true, false) = true f2(false, true) = false f2(true, true) = false f3(false, false) = false f3(true, false) = false f3(false, true) = false f3(true, true) = true f4(false, false) = false f4(true, false) = true f4(false, true) = true f4(true, true) = false
OK, let’s conclude with one more spec:
spec(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = (NOT (b0 AND ((b1 OR b2) XOR b3)) AND b4) XOR b5;
This is implementable by f, and SAL returns
f0 = Eqv f1 = OrNot f2 = And f3 = Eqv f4 = Nor
Although these assignments compute the same function, they differ from those in our specification. Just to double-check, we can ask SAL if they’re equivalent:
spec1(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = ((b0 AND ((NOT (b1 OR b2)) b3)) OR NOT b4) b5;
specifies the assignments returned, and
eq: THEOREM m |- spec(b0, b1, b2, b3, b4, b5) = spec1(b0, b1, b2, b3, b4, b5);
asks if the two specifications are equivalent. They are.
“Schrodinger’s Probability” for Error-Checking Codes
Posted: May 15, 2009 Filed under: Fault Tolerance, Software | Tags: Byzantine fault, CRC, Fault Tolerance, Haskell 2 Comments »In a previous post, I discussed the notion of Schrödinger CRCs, first described by Kevin Driscoll et al. in their paper Byzantine Fault Tolerance, from Theory to Reality. The basic idea is that error-detecting codes do not necessarily prevent two receivers from obtaining messages that are semantically different (i.e., different data) but syntactically valid (i.e., the CRC matches the respective data words received). The upshot is that even with CRCs, you can suffer Byzantine faults, with some probability.
… So what is that probability of a Schrödinger’s CRC? That’s the topic of this post—which cleans up a few of the ideas I presented earlier. I published a short paper on the topic, which I presented at Dependable Sensors and Networks, 2010, while Kevin Driscoll was in the audience! If you’d prefer to read the PDF or get the slides, they’re here. The simulation code (Haskell) is here.
