Design Automation Engineer Leior Varon has been poking around at Free & Fair recently and offered to reflect on what he’s been learning. Varon has a background in electrical engineering, but became interested in F&F’s use of formal methods in software system design. So, in order to get his feet wet in this world, Varon spent 6 weeks creating and implementing the formal specifications for Qubie, our Poll Queue Monitor. Here are his reflections.

My first taste of formal software methods

Abstract

Formal software methods are mathematically based techniques that can give mathematical proof of correctness and security. But what does that really mean? How does it compare to traditional test based verification? What background is needed in order to successfully make use of formal methods on software projects? I spent the last 6 weeks finding out…

My background

I know a lot about traditional test based verification techniques from my background as an electrical engineer working on complex integrated circuits (ASICs) but this was my first time learning and utilizing formal methods.

The task

I worked on the Qubie project: a small, portable, computer that uses public wireless signals to measure how long voters wait in line to cast their ballots. Voter privacy is essential so all sensitive information must be securely and verifiably protected.

The methods

Traditional methods entail writing numerous unit tests to try and capture each feature and each possibility of the system. Done correctly, this method can give a good assurance that the system works as specified but it does not give absolute certainty:

  •         Only a small fraction of possibilities are tested.
  •         There is no way to determine if a critical test is missing.
  •         There may be bugs or holes in the specification.

The method chosen for Qubie is a formal method called “Design by Contract”. All the interactions between the various parts of the system are described as contracts which are broken down into logical equations that can be solved by tools to give mathematical proof of correctness.

The tools

The specifications were written in Extended Business Object Notation (BON) with the help of the eclipse BONc plugin. The program was implemented in Verifiable C (a subset of C) using the eclipse C/C++ EDA. The formal proof of correctness was done with functional specifications using the frama-c Weakest Precondition (WP) plugin. The program was compiled with gcc on a linux ubuntu virtual machine.

The process

The first stage was to divide the product into its high level blocks and define the interactions between the blocks. These features were written in plain English to form an informal specification. In the case of Qubie I began with a fully defined Informal specification. Below is a snippet with reduced features for the sake of clarity:

Informal Specification

class_chart QUBIE
explanation
 “Qubie is a passive, privacy-preserving monitoring system that records\
\ contacts with WiFi devices in its vicinity. When used in a polling place\
\ or other location, its observations can provide information about queue\
\ lengths and other characteristics of the environment.”
query
 “Are you running?”
command
 “Start running!”,
 “Stop running!”
constraint
 “Once a Qubie is stopped, it cannot be restarted.”
end

I refined the informal specification into a formal specification by writing each informal sentence in BON syntax and adding the contracts involved with each feature.

Formal Specification

class QUBIE
  feature
              running : BOOLEAN
                    ensure Result = (state = running) end
              start_running
                    require
                          booting
                    ensure
                          state = running;
                              action_published(state);
                    end
              stop_running
                    require running
                    ensure
                          state = stopped;
                              action_published(state);
                    end
        end

The formal specification also includes additional sections such as a static model to create diagrams that indicate relationships between different parts of the system and a dynamic model that expresses scenarios as a sequence of events.

The features in the formal specification were then converted into function headers or ACSL predicates and the requirements and assurances were converted into ACSL annotations:

Implementation

/*@ ensures \result == (the_qubie_state == RUNNING);
assigns \nothing;
*/
bool running();
/*@ requires (the_qubie_state == POWERED_ON);
ensures (the_qubie_state == BOOTING);
ensures logical_published(BOOTING);
*/
void start_booting;
/*@ requires (the_qubie_state == BOOTING);
ensures (the_qubie_state == RUNNING);
ensures logical_published(RUNNING);
*/
void start_running;

The hard work was done in the specification stage so implementing individual functions was relatively simple. I spent more time than I’d like to admit on minutia related to C syntax and flattening out object oriented concepts into C language but by the time the program compiled it took almost no time to get it running.

The last stage was to compile the annotations with frama-c and to prove the correctness of the program. For example to prove that the start_booting function can only be called when the_qubie_state == POWERED_ON and that by the time the function returns, the_qubie_state has always been changed to BOOTING.

The results

I spent about 6 weeks working on Qubie software:

  •         1 week to learn BON
  •         1-2 weeks to create the formal bon specification
  •         2-3 weeks to implement the main features, compile and run a few dynamic tests.
  •         1 week to compile and prove 67% of the frama-c WP goals.

Unfortunately I ran out of time before being able to refine the code and prove 100% of the WP goals but the process of writing the frama-c notations revealed a number of bugs that would have otherwise only been caught in run time.

Thoughts

Like me, anyone with good analytical skills and a good programming background can learn to use formal methods without prior experience. Formal methods are not “magic”, the process involves thought and effort especially in order to reach 100% certainty. That effort, however, truly gives a level of certainty that cannot be reached with traditional methods.

I did not find any active online communities that deal with BON specifications but the book “Seamless Object-Oriented Software Architecture” is available online for free and parts II and III are very thorough and helpful.  There are plenty of tutorials and communities for helping with C and frama-c questions.

There were some areas where automated tools could have given great benefit, especially when fixing specification bugs during the implementation stage to ensure the BON specification doesn’t diverge from the implementation. In this case some creative grep and sed commands were enough to proceed.

I had fun working on Qubie and learning formal methods. As the need for certainty and security increases I look forward to having more opportunities to use these new tools.