Safe and Secure Software Systems An Automated Reasoning Perspective Andrew Ireland Dependable Systems Group School of Mathematical & Computer Sciences Heriot-Watt University Edinburgh Setting the Scene Inaugural lecture? Achievements and research vision Blend of technical and big picture coupled

historical perspective First things first software and automated reasoning? Making Stuff and How it Works Making Software Stuff - Data Numbers: Lists:

Making Software Stuff - Data Empty list is represented by the constant Non-empty list is constructed using the operator (pronounced cons) Example, the list even numbers [ 0, 2, 4, 6, 8 ] is represented by 0 :: (2 :: (4 :: (6 :: (8 :: )))) Making Software Stuff Programs

Gluing lists together : Reversing a list Program Execution program data [ 1, 2, 3 ] ( [ , , ] )

[ , , ] How It Works ( [ , , ] ) [ , , ] A Practical Example

( ( [ ] ) ) Proving Stuff Proof = Guarantee + Explanation Proving the conjecture: Givens Goal All Sylvanians are tiny, Coral is a Sylvanian therefore Coral is tiny

Coral is tiny? (conjecture) Automated Reasoning: building software systems that construct proofs Proof as Guarantee Givens Goal Proof as Guarantee

Givens Goal Proof as Guarantee Givens Goal Proof as Guarantee Givens

Goal Proof as Guarantee Givens Goal Proof as Guarantee Givens Goal

Proof as Guarantee Givens Goal Proof as Guarantee Givens Goal Proof as Guarantee Givens

Goal Proof as Guarantee Givens Goal Proof as Guarantee Proof by Mathematical Induction essential for reasoning about recursion, iteration, feedback loops

List induction - to prove : prove assume then prove Conjecture: (base case) (step case) Proof as Guarantee Given: Goal:

( ) ( ) @ ( ( @ ( ) ) ( ) ( = ) ( = ) Proof as Explanation Given: Goal: Proof as Explanation Given:

Goal: Proof as Explanation Given: Goal: ( ) ( ) @ ( Proof as Explanation Given: Goal: ( ) ( ) @ (

Proof as Explanation Given: Goal: ( ) ( ) @ ( Proof as Explanation Given: Goal: ( ) ( ) @ ( ( @ ( ) ) ( )

Proof as Explanation Given: Goal: ( ) ( ) @ ( ( @ ( ) ) ( ) Proof as Explanation Given: Goal: ( ) ( ) @ (

( @ ( ) ) ( ) ( = ) ( = ) Proof as Explanation Given: Goal: ( ) ( ) @ ( ( @ ( ) ) ( ) ( = ) ( = )

Rippling = difference identification + difference reduction Proof Plans A proof plan represents a common pattern of reasoning, e.g. rippling Proof plan = tactic + strategy Guarantee Explanation Proof plans:

Automate the search for proofs - via proof planning Promote strategy reuse Proof Planning Conjecture Theory Method Strategies

Tactic [ tailored for conjecture ] Proof Planning Conjecture Theory Critic Method

Strategies Critics provide flexibility during the search for proofs Productive Use of Failure Conjecture Generalization MissingDProperties (Lemmas)

Ripple Ripple method method Case Splits Induction Rules Making Software Stuff Reversing a list

Reversing a list - Faster! Conjecture Generalization Critic . Given: ( ) = ( , ) Goal: ( h )= ( h , ) Proof-failure Analysis:

blocked ( , ) ( , ) matching rule, i.e. missing universally quantified variable in conjecture, i.e. Conjecture Generalization Critic , .: ( ) . ( ) @ = ( , ) ( , ) = [email protected] ( )= ? Given:

( () ).. ) , = )= :: )@ = )) ) ) )@

( (h( ( (,(, ,( h Goal: ( ) , = ) = ( h( h , ,( ) ) ) ( h( h) @ proof planning ( ) @ h = ( , h )

Conjecture Generalization Critic , : ( ) . ( ) @ = ( , ) ( , ) = @ ( )= Given: ( ) @ h = ( , h ) Goal: ( h ) @ = ( h , ) proof planning (

) @ h = ( , h ) http://www.rippling.org/ Related PhD Projects Proof planning for imperative program development (Jamie Stark) Reuse of proof plans Loop invariant discovery Program synthesis, i.e. ... develop a program and its proof hand-in-hand, with the proof ideas Leading the way! (Gries, 1981)

Bertha Related PhD Projects Using Proof in Transformation Synthesis for Automatic Parallelisation - EPSRC GR/L42889 (Andrew Cook) Verification & synthesis of performance enhancing eureka steps, e.g. transformations that facilitate the parallelization of software Reasoning About Correctness Properties of a

Coordination Programming Language (Gudmund Grov) HUME: a novel programming language Verification and transformation of HUME programs to improve resource usage (space and time guarantees) Alan Turing: 1912-1954 Software Verification Birth of the Modern Computer

Manchesters Small Scale Experimental Machine Turing, Turing,A. A. M. M. 1949. 1949. A.K.A. The Baby (1948) Checking Checking aa Large Large Routine. Routine.

In In Report Report of of aa Conference Conference on on High High Speed Speed Automatic Automatic Calculating Calculating Machines, Machines, Univ.

Univ. Math. Math. Lab., Lab., Cambridge, Cambridge, pp. pp. 67-69. 67-69. And 63 Years Later ? A wealth of new logics and automated reasoning techniques Computers are faster and memory is cheap

Verification tools are typically highly integrated and automatic Significant industrial scale success stories within niche markets, e.g. Microsoft, Praxis, D-RisQ, Now it matters! Now it Matters! Software is woven into almost all aspects of our daily lives from communications, entertainment and consumer electronics, to finance, defence and national infrastructure A key differentiator in commercial products is embedded software dependability is crucial to commercial success,

where software correctness is a key ingredient Cyber Security carries significant risks for economic growth and society in general a priority area for UK Government Software testing is not enough to guarantee safe and secure software systems correctness-by-construction is called for, underpinned by a range of formal notations and automated reasoning technologies International Verified Software Initiative coming together of academia and industry SPARK Programming Language SPARK is an Ada subset that eliminates potential

ambiguities and insecurities (Altran Praxis) Expressive enough for industrial applications, but restrictive enough to support rigorous analysis, i.e. correctness-by-construction Applications: e.g. air traffic control (iFACTS), avionics (Eurofighter Typhoon), security (Mondex), Focus on exception freedom proof, e.g. proving code is free from arithmetic overflows, buffer overflows, division by zero, .

Arithmetic Overflow Consider converting 64-bits of data into 16-bits: Overflow Error The Cost of Failure Developed by European Space Agency Unmanned rocket with a cargo of scientific satellites ($500 million) In 1996, just 39 seconds into its maiden flight an overflow error occurred resulting the Ariane 5 control software initiating a self-destruction operation!

Ariane 5 Verifying SPARK Code SPARK code SPARK Examiner VCs

SPADE Simplifier Proofs Unproven VCs Cmds Annotations

SPADE Proof Checker VCs = Verification Conditions (conjectures) Our focus was on the problems the SPARK tools failed on: Verifying loops (iteration) Loop invariant discovery productive use of failure Proof Planning for SPARK SPARK code

SPARK Examiner VCs SPADE Simplifier Proofs

Unproven VCs Cmds SPADEase Annotations SPADE Proof Checker Bill J. Ellis (RA + PhD) EPSRC Critical Systems programme (GR/R24081) EPSRC RAIS Scheme (GR/T11289)

http://www.macs.hw.ac.uk/nuspade SPADEase subtype AR_T is Integer range 0..9; type A_T is array (AR_T) of Integer; ... procedure Filter(A: in A_T; R: out Integer)is begin R:=0; for I in AR_T loop --# if A(I)>=0

assert Rand >= A(I)<=100 0 and R <=then I*100 if A(I)>=0 R:=R+A(I); and A(I)<=100 then end if; R:=R+A(I); end end loop; if;

endend Filter; loop; end Filter; Unproven VCs RAbstract >= ? and R <= ? Predicates

Program Analyzer Annotations --# assert R >= 0 and R <= I*100 Proof Planner SPADEase Impact? It increases the proportion of SPARKgenerated verification conditions that can be

proved automatically without introducing any new opaque, black-box processes. Peter Amey Chief Technical Officer Praxis High Integrity Systems SPADEase Impact? The separation of proof planning from proof checking also acts as a talent multiplier by allowing proof experts to spend their time creating new and reusable methods and

approaches rather than working on individual proofs. Peter Amey Chief Technical Officer Praxis High Integrity Systems Going Beyond Exception Freedom Reasoning about the functional correctness of pointer programs proving that the code does the right thing Separation Logic: Adapted the rippling proof plan Extended work on automated invariant discovery

Ewen Maclean, Gudmund Grov (RAs), Richard Addison (MEng) EPSRC funding: EP/F037597 and Platform Grant EP/J001058 www.macs.hw.ac.uk/core Tech Talks at Google via Beyond Code Level Analysis Sensor:= Brakes.Activate; Sensor:= Brakes.Activate; Active:= False; Active:= False; end if;

end if; else else Alarm.Enable; Alarm.Enable; end if; end if; else else if Alarm.Enabled then if Alarm.Enabled then Alarm.Disable;

Alarm.Disable; end if; end if; end if; end if; end if; end if; else else if Reset.Enabled then if Reset.Enabled then Alarm.Disable;

Alarm.Disable; Brakes.Deactivate; Brakes.Deactivate; Speed:= 0; Speed:= 0; Active:= True; Active:= True; end if; end if; end if; end if; end Control;

end Control; end ATP; end ATP; Requirements Rajiv Murali (PhD) EPSRC & BAE Systems Formal Design Models Formal

Design Models Teresa Llano (PhD) EPSRC & BAE Systems Code Reasoned Modelling Reasoning Modelling

Combine common patterns of reasoning with common patterns of modelling (design) Abstract away from low-level proof-failures, and automatically provide high-level guidance to designers Accessibility and productivity allow creative designers to make better use of their time Reasoned Modelling Reasoning Modelling

Gudmund Grov, Teresa Llano (PhD), Alison Pease Collaboration with Edinburgh University & Imperial College: System Design, Cognitive Modelling, AI Problem Solving Event-B (Rodin toolset) Bosch, Siemens, SAP, Funding: EPSRC EP/F037058, EP/J001058, BAE Systems www.macs.hw.ac.uk/remo/ A Longer-term Vision Reasoning Software System DesignModelling

Environments Embed Reasoned Modelling within conventional design tools Knowledge Transfer ITI Techmedia (Scottish Enterprise) Software Integrity Engineering Programme Ewen Maclean, Gudmund Grov, Andrew Cook (RAs) BAE Systems (Warton) A case study in reasoned modelling Teresa Llano (RA)

Altran Praxis Critical Blue BAE Systems Bill Ellis (PhD) Andrew Cook (PhD) Ben Gorry (PhD) Conclusion Unsafe and insecure software can have a massive impact on economies and society in

general Automated reasoning has an unique role to play in the development of safe and secure software As the sophistication and reach of software systems increases, so will the importance of automated reasoning As computer scientists we are challenged by a grand opportunity! Thank You!