Guest Lectures

K. Rustan M. Leino, Senior Principal Applied Scientist at Amazon Web Services

Guest Lectures

K. Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services.

Leino is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

Guest Lectures

Wolfgang Ahrendt, Professor of Computer Science at Chalmers University of Technology

Guest Lectures

Wolfgang Ahrendt is a Professor of Computer Science at Chalmers University of Technology, Sweden. He is one of the Staff Group Leaders in the KeY project.

He is an expert in automated theorem proving, as well as software verification and specification. He is currently developing methods to verify blockchain smart contracts.

Guest Lectures

Bart Jacobs, Associate Professor at the Department of Computer Science of KU Leuven

Guest Lectures

Bart Jacobs is an associate professor at the Department of Computer Science of KU Leuven - University of Leuven, Belgium. He is a member of the Security: Programming Languages task force of the imec-DistriNet research group.

After contributing to Spec# as an intern with Wolfram Schulte and Rustan Leino at Microsoft Research Redmond, he has been developing VeriFast since 2008.

Focus: Program Verification

• In particular, we will focus on design by contract and deductive verification
• Design by contract is an approach to design software that prescribes the use of formal, precise and verifiable specifications for software components, extending the ordinary definition of abstract data types with preconditions, postconditions and invariants.

Focus: Program Verification

• Deductive software verification is the process of turning the correctness of a program into a mathematical statement and then proving it.
• We'll use Dafny extensively, an automatic program verifier.

Goal: reduce the number of bugs in a given program

Dijkstra on the term 'bug'

“We could, for instance, begin with cleaning up our language by no longer calling a bug a bug but by calling it an error. It is much more honest because it squarely puts the blame where it belongs, viz. with the programmer who made the error.” (EWD 1036)

Edsger W. Dijkstra (1930 - 2002)

Question: what is the most used approach to reduce the number of bugs in software?

Answer: Software testing.

Testing vs. Verification

“Program testing may convincingly demonstrate the presence of bugs, but can never demonstrate their absence.” (EWD 1036)

Edsger W. Dijkstra (1930 - 2002)

Assertion Based Verification

“It may be true, that whenever C actually reaches a certain point in the flow diagram, one or more bound variables will necessarily possess certain specified values, or possess certain properties, or satisfy certain relations with each other. Furthermore, we may, at such a point, indicate the validity of these limitations. For this reason we will denote each area in which the validity of such limitations is being asserted, by a special box, which we call an assertion box.” (1947)

Herman Goldstine (1913 - 2004)

John von Neumann (1903 - 1957)

Assertion Based Verification

“How can one check a routine in the sense of making sure that it is right?

In order that the man who checks may not have too difficult a task the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole programme easily follows. ” (24 June 1949)

Alan Turing (1912 - 1954)

Assertion Based Verification

“ The basis of our approach is the notion of an interpretation of a program: that is, an association of a proposition with each connection in the flow of control through a program, where the proposition is asserted to hold whenever that connection is taken. ” (1967)

Robert Floyd (1936 - 2001)

Assertion Based Verification

“The intended function of a program, or part of a program, can be specified by making general assertions about the values which the relevant variables will take after execution of the program. These assertions will usually not ascribe particular values to each variable, but will rather specify certain general properties of the values and the relationships holding between them.” (October 1969)

Sir Tony Hoare (1934 - )

What is the current practice in Software Engineering?

The Software Process

• A structured set of activities required to develop a software system.
• Many different software processes but all involve:
  • Specification – defining what the system should do;
  • Design and implementation – defining the organization of the system and implementing the system;
  • Validation – checking that it does what the customer wants;
  • Evolution – changing the system in response to changing customer needs.

Software Specification

Customers and engineers define the software that is to be produced and the constraints on its operation.

Example: suppose the goal is to build a swing

Requirements Engineering

Process of understanding and defining what services are required from the system and identifying the constraints on the system's operation and development.

Requirements Engineering Process

Goal: produce agreed requirements document that specifies a system satisfying stakeholder requirements

Usually, performed at two levels: end-users and clients and developers

Four main activities:

1. Feasibility study
   • Is it technically and financially feasible to build the system?
2. Requirements elicitation and analysis
   • What do the system stakeholders require or expect from the system?
3. Requirements Specification
   • Defining the requirements in detail
4. Requirements Validation
   • Checking the validity of the requirements

(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Why bother?

Because we want to build dependable systems.

System dependability

• For many computer-based systems, the most important system property is the dependability of the system.
• The dependability of a system reflects the user’s degree of trust in that system. It reflects the extent of the user’s confidence that it will operate as users expect and that it will not ‘fail’ in normal use.
• Dependability covers the related systems attributes of reliability, availability and security. These are all inter-dependent.

Importance of dependability

• System failures may have widespread effects with large numbers of people affected by the failure.
• Systems that are not dependable and are unreliable, unsafe or insecure may be rejected by their users.
• The costs of system failure may be very high if the failure leads to economic losses or physical damage.
• Undependable systems may cause information loss with a high consequent recovery cost.

Causes of failure

• Hardware failure
  • Hardware fails because of design and manufacturing errors or because components have reached the end of their natural life.
• Software failure
  • Software fails due to errors in its specification, design or implementation.
• Operational failure
  • Human operators make mistakes. Now perhaps the largest single cause of system failures in socio-technical systems.

Principal dependability properties

(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Principal properties

• Availability
  • The probability that the system will be up and running and able to deliver useful services to users.
• Reliability
  • The probability that the system will correctly deliver services as expected by users.
• Safety
  • A judgment of how likely it is that the system will cause damage to people or its environment.
• Security
  • A judgment of how likely it is that the system can resist accidental or deliberate intrusions.

Reliability in use

• Removing X% of the faults in a system will not necessarily improve the reliability by X%. A study at IBM showed that removing 60% of product defects resulted in a 3% improvement in reliability (Mills et al. 1987).
• Program defects may be in rarely executed sections of the code so may never be encountered by users. Removing these does not affect the perceived reliability.
• A program with known faults may therefore still be perceived as reliable by its users.

Reliability achievement

• Fault avoidance
  • Development techniques are used that either minimise the possibility of mistakes or trap mistakes before they result in the introduction of system faults.
• Fault detection and removal
  • Verification and validation techniques that increase the probability of detecting and correcting errors before the system goes into service are used.
• Fault tolerance
  • Run-time techniques are used to ensure that system faults do not result in system errors and/or that system errors do not lead to system failures.

Safety and Reliability

• Safety and reliability are related but distinct
  • In general, reliability and availability are necessary but not sufficient conditions for system safety
• Reliability is concerned with conformance to a given specification and delivery of service
• Safety is concerned with ensuring system cannot cause damage irrespective of whether or not it conforms to its specification

Risk analysis is important in the specification of security and dependability requirements

Risk-driven specification

• Critical systems specification should be risk-driven.
• This approach has been widely used in safety and security-critical systems.
• The aim of the specification process should be to understand the risks (safety, security, etc.) faced by the system and to define requirements that reduce these risks.

Stages of risk-based analysis

• Risk identification
  • Identify potential risks that may arise.
• Risk analysis and classification
  • Assess the seriousness of each risk.
• Risk decomposition
  • Decompose risks to discover their potential root causes.
• Risk reduction assessment
  • Define how each risk must be taken into eliminated or reduced when the system is designed.

The risk triangle

ALARP: As low as reasonably practical
(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Hazard analysis

• Concerned with discovering the root causes of risks in a particular system.
• Techniques have been mostly derived from safety-critical systems and can be:
  • Inductive, bottom-up techniques. Start with a proposed system failure and assess the hazards that could arise from that failure.
  • Deductive, top-down techniques. Start with a hazard and deduce what the causes of this could be.

Fault-tree analysis

Widely-used approach to hazard analysis: fault trees.

• A deductive top-down technique.
• Put the risk or hazard at the root of the tree and identify the system states that could lead to that hazard.
• Where appropriate, link these with ‘and’ or ‘or’ conditions.
• A goal should be to minimise the number of single causes of system failure.

Example: Insulin Pump

Source: medtruth.

(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Fault-tree analysis

• Three possible conditions that can lead to delivery of incorrect dose of insulin
  • Incorrect measurement of blood sugar level
  • Failure of delivery system
  • Dose delivered at wrong time
• By analysis of the fault tree, root causes of these hazards related to software are:
  • Algorithm error
  • Arithmetic error

Risk reduction

• The aim of this process is to identify dependability requirements that specify how the risks should be managed and ensure that accidents/incidents do not arise.
• Risk reduction strategies
  • Risk avoidance;
  • Risk detection and removal;
  • Damage limitation.

Insulin pump: software risks

• Arithmetic error
  • A computation causes the value of a variable to overflow or underflow.
  • Maybe include an exception handler for each type of arithmetic error.
• Algorithmic error
  • Compare dose to be delivered with previous dose or safe maximum doses. Reduce dose if too high.

How do you convince a client that a given system is dependable?

Safety and dependability cases

• Safety and dependability cases are structured documents that set out detailed arguments and evidence that a required level of safety or dependability has been achieved.
• They are normally required by regulators before a system can be certified for operational use. The regulator’s responsibility is to check that a system is as safe or dependable as is practical.

The system safety case

• A safety case is:
  • A documented body of evidence that provides a convincing and valid argument that a system is adequately safe for a given application in a given environment.
• Arguments in a safety or dependability case can be based on formal proof, design rationale, safety proofs, etc. Process factors may also be included.
• A software safety/dependability case is part of a wider system safety/dependability case.

Structured arguments

• Safety/dependability cases should be based around structured arguments that present evidence to justify the assertions made in these arguments.
• The argument justifies why a claim about system safety/security is justified by the available evidence.
• Arguments are based on claims and evidence.

(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Insulin pump safety argument

• Insulin pump safety:
  • Claim: The maximum single dose of insulin to be delivered (CurrentDose) will not exceed MaxDose.
  • Evidence: Safety argument for insulin pump (discussed later)
  • Evidence: Test data for insulin pump. The value of currentDose was correctly computed in 400 tests
  • Evidence: Static analysis report for insulin pump software revealed no anomalies that affected the value of CurrentDose
  • Argument: The evidence presented demonstrates that the maximum dose of insulin that can be computed = MaxDose.

Structured safety arguments

• Structured arguments that demonstrate that a system meets its safety obligations.
• It is not necessary to demonstrate that the program works as intended; the aim is simply to demonstrate safety.
• Generally based on a claim hierarchy.
  • You start at the leaves of the hierarchy and demonstrate safety. This implies the higher-level claims are true.

A safety claim hierarchy for the insulin pump

(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Safety arguments

• Safety arguments are intended to show that the system cannot reach an unsafe state.
• These are weaker than correctness arguments which must show that the system code conforms to its specification.
• They are generally based on proof by contradiction
  • Assume that an unsafe state can be reached.
  • Show that this is contradicted by the program code.
• A graphical model of the safety argument may be developed.

Construction of a safety argument

• Establish the safe exit conditions for a component or a program.
• Starting from the END of the code, work backwards until you have identified all paths that lead to the exit of the code.
• Assume that the exit condition is false.
• Show that, for each path leading to the exit that the assignments made in that path contradict the assumption of an unsafe exit from the component.

Insulin dose computation

-- The insulin dose to be delivered is a function of blood sugar level, 
-- the previous dose delivered and the time of delivery of the previous dose

currentDose = computeInsulin();
// Safety check—adjust currentDose if necessary. 
// if statement 1
if (previousDose == 0) {
    if (currentDose > maxDose/2) { currentDose = maxDose/2; }
} else if (currentDose > (previousDose*2)) { currentDose = previousDose*2; }
// if statement 2
if ( currentDose < minimumDose ) { currentDose = 0; }
else if ( currentDose > maxDose ) { currentDose = maxDose; }
administerInsulin(currentDose);

(Sommerville, Ian. Software engineering. Addison-Wesley/Pearson, 2011.)

Program paths

• Neither branch of if-statement 2 is executed
  • Can only happen if CurrentDose is >= minimumDose and <= maxDose.
• then branch of if-statement 2 is executed
  • currentDose = 0.
• else branch of if-statement 2 is executed
  • currentDose = maxDose.
• In all cases, the post conditions contradict the unsafe condition that the dose administered is greater than maxDose.

Verification and Formal Methods

• Formal methods can be used when a mathematical specification of the system is produced.
• They are the ultimate static verification technique that may be used at different stages in the development process:
  • A formal specification may be developed and mathematically analyzed for consistency. This helps discover specification errors and omissions.
  • Formal arguments that a program conforms to its mathematical specification may be developed. This is effective in discovering programming and design errors.

Arguments for formal methods

• Producing a mathematical specification requires a detailed analysis of the requirements and this is likely to uncover errors.
• They can detect implementation errors before testing when the program is analyzed alongside the specification.
• Concurrent systems can be analysed to discover race conditions that might lead to deadlock. Testing for such problems is very difficult.

Arguments against formal methods

• Require specialised notations that cannot be understood by domain experts.
• Very expensive to develop a specification and even more expensive to show that a program meets that specification.
• Proofs may contain errors.
• It may be possible to reach the same level of confidence in a program more cheaply using other V & V techniques.

Automated static analysis

• Static analysers are software tools for source text processing.
• They parse the program text and try to discover potentially erroneous conditions and bring these to the attention of the V & V team.
• They are very effective as an aid to inspections: they are a supplement to but not a replacement for inspections.

Levels of static analysis

• Characteristic error checking
  • The static analyzer can check for patterns in the code that are characteristic of errors made by programmers using a particular language.
• User-defined error checking
  • Users of a programming language define error patterns, thus extending the types of error that can be detected. This allows specific rules that apply to a program to be checked.
• Assertion checking
  • Developers include formal assertions in their program and relationships that must hold. The static analyzer symbolically executes the code and highlights potential problems.

Use of static analysis

• Particularly valuable when a language such as C is used which has weak typing and hence many errors are undetected by the compiler.
• Particularly valuable for security checking: the static analyzer can discover areas of vulnerability such as buffer overflows or unchecked inputs.
• Static analysis is now routinely used in the development of many safety and security critical systems.

Design by Contract (DbC)

• Design By Contract (DbC) is a software correctness methodology
• Term coined by Bertrand Meyer; central concept in the Eiffel programming language
• A contract can be summarised by the "three questions" that the designer must repeatedly answer in the contract:
  • What does the contract expect?
  • What does the contract guarantee?
  • What does the contract maintain?

Design by Contract (DbC)

• Language support for contracts exists in different forms:
  • Natively: Eiffel, Racket, SPARK Ada, Dafny, ...
  • Third-party: JML for Java; Spec# for C#; PyContracts for Python; ...

Design by Contract (DbC)

Here's an example of contracts in Eiffel:

deposit (sum: INTEGER) is
            -- Deposit sum into the account.
         require
            sum >= 0
         do
            add (sum)
         ensure
            balance = old balance + sum
        end

Design by Contract (DbC)

Here's an example of contracts in Java (OpenJML):

public class Subtract {
    //@ requires a > 0;
    //@ requires b > 0;
    //@ ensures \result == a-b;
    public static int subtract(int a, int b){
        return a-b;
    }

    public static void main(String args[]){
        System.out.println(subtract(2,3));
    }
}