Software Bugs and Formal Verification in Critical Systems

Software bugs have caused catastrophic events like radiation overdoses and rocket explosions, emphasizing the importance of formal verification in ensuring software correctness. Formal verification uses mathematical models to prove software correctness, offering higher assurance, especially in safety-critical systems. The advancement in automated reasoning is enhancing the automation and scalability of proof techniques. The use of formal verification is crucial for rectifying bugs and preventing potential disasters in critical systems.

• Software Bugs
• Formal Verification
• Critical Systems
• Safety-Critical Applications
• Automated Reasoning

jama_ico Follow

Uploaded on Sep 13, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Verification of Neural Networks Clark Barrett, Stanford University 1 / 27

2. Therac-25 Between 1985 and 1987, at least 6 accidental radiation overdoses were administered. All the victims were injured, and 3 of them later died. 2 / 27

3. Ariane 5 Rocket On June 4, 1996, an unmanned Ariane 5 rocket launched by the European Space Agency exploded just 40 seconds after its lift-off. Value of rocket and cargo: $500 million 3 / 27

4. Blackout In August, 2003, the largest blackout in our country s history occurred. Estimated cost to New York City alone: $1.1 billion. 4 / 27

5. What do these events have in common? Caused by Software Bugs! Each of the overdoses from the Therac-25 was the result of a bug in the controlling software. The Ariane 5 explosion was the result of an unsafe floating point to integer conversion in the rocket s software system. A software bug caused an alarm system failure at FirstEnergy in Akron, Ohio. An early response to those alarms would likely have prevented the blackout. 5 / 27

6. Formal Verification Good software engineering practices can eliminate many but not all bugs Formal verification can be used to mathematically prove that a piece of software is correct. [Formal] software verification has been the Holy Grail of computer science for many decades Bill Gates Formal verification can be costly in terms of time and effort, but the extra assurance may be worth it, especially for safety-critical systems. 6 / 27

7. What is Formal Verification? Create a mathematical model of the system An inaccurate model can introduce or mask bugs. Fortunately, this can often be done automatically. Specify formally what the properties of the system should be Prove that the model has the desired properties Much better than any testing method Covers all possible cases Good news: Recent advances in automated reasoning are improving the automation and scalability of proof techniques 7 / 27

8. AI Systems What about software with AI components, deep neural networks, for example? Many traditional software engineering techniques (e.g. code reviews, checking code coverage, assertions, modular programming, etc.) are not applicable How do we ensure such systems are safe and correct, especially when used in safety- or mission-critical applications? Can we use formal verification on such systems? 8 / 27

9. Example: ACAS Xu Airborne Collision-Avoidance System for drones A new standard being developed for the FAA Produce advisories: 1. Strong left (SL) 2. Weak left (L) 3. Strong right (SR) 4. Weak right (R) 5. Clear of conflict (COC) One high-performing implementation uses deep neural networks Can we verify it? 9 / 27

10. Verifying Neural Networks Step 1: Create a mathematical model of the neural network 11 / 27

11. Deep Neural Networks (DNNs) Steps: 1. 2. Weighted sum Activation function 2 1 3 2 1 + 0 3 + ( 1) 2 = 4 0 ?(4) 2 1 12 / 27

12. Rectified Linear Units (ReLUs) ReLU(?) = max(0,?) ? 0: active case, return ? ? < 0: inactive case, return 0 2 1 1 3 1 1 + 2 3 + 0 2 = 5 2 1 + 0 3 + ( 1) 2 = 4 2 0 4 0 2 1 0 13 / 27

13. A Simple Example ?2 1 1 ?1 ?4 1 1 ?3 14 / 27

14. Modeling Networks Introduce equalities: ?2 ?3 ?4 ?3 ReLU ? ? ?2 ?2 1 1 ? ?1= 0 ?+ ?1= 0 ? ?2 ?1 ?4 ?= 0 ReLU 1 1 ? ? ?3 ?3 Set bounds: ?2 ?2 ?,?3 ?,?3 ? ( , ) ? 0, Special ReLU constraints: ?2 ?3 ?= ???(?2 ?= ???(?3 ?> 0,?2 ?> 0,?3 ?,0) ?,0) 15 / 27

15. Verifying Neural Networks Step 2: Formally specify the properties of the system 16 / 27

16. A Simple Example ?2 1 1 ?1 ?4 1 1 ?3 Property being checked: If ?1 [0,1] then ?4 [0.5,1]? 17 / 27

17. Encoding Networks Introduce equalities: ?2 ?3 ?4 ?3 ReLU ? ? ?2 ?2 1 1 ? ?1= 0 ?+ ?1= 0 ? ?2 ?1 ?4 ?= 0 ReLU 1 1 ? ? ?3 ?3 Set bounds: ?1 [0,1] ?4 0.5,1 ?2 ?2 ?,?3 ?,?3 ? ( , ) ? 0, Special ReLU constraints: ?2 ?3 ?= ???(?2 ?= ???(?3 ?> 0,?2 ?> 0,?3 ?,0) ?,0) 18 / 27

18. Verifying Neural Networks: Specification Challenges System-level specification (e.g. the airplane does not crash) vs property on the neural network Property may not be formally specifiable (e.g. the network correctly identifies cats as cats) May not have any specification at all 19 / 27

19. Verifying Neural Networks: Specification A first step: local robustness Local robustness is a property that can be checked for any network Check that in some small neighborhood of a known test point, the network behaves similarly to the test point Formally, network ? is ?-locally-robust at ?0 if: ?. ? ?0 ? ? ? = ? ?0 20 / 27

20. Local Robustness: Example Network ? is ?-locally-robust at ?0 if: ?. ? ?0 ? ? ? = ? ?0 ?0 21 / 27

21. Verifying Neural Networks Step 3: Prove that the system satisfies the properties 22 / 27

22. Verifying Neural Networks: Proving Properties Need a proof engine that can reason about: Linear arithmetic over real numbers Limited non-linearity (activation functions) Off-the-shelf solutions: Mixed-integer linear programming (e.g. gurobi) SMT solvers (e.g. CVC4, Z3) Problem: off-the-shelf solvers can t handle activation constraints efficiently 23 / 27

23. Verifying Neural Networks: Proving Properties Exciting new research area: specialized solvers/techniques for verifying neural networks Various techniques being proposed and developed: Reachability, Search, Optimization Significant speed-ups from parallelization (splitting input space) Overview at https://arxiv.org/abs/1903.06758 24 / 27

24. Marabou An open-source research platform for experimenting with formal verification techniques for neural networks Custom linear-programming engine Support for piece-wise linear functions (e.g. ReLU, max) Accepts several input formats (e.g. TensorFlow) Parallelization via divide-and-conquer mode Network-level pruning and propagation techniques SMT-based search management https://github.com/guykatzz/Marabou 25 / 27

25. Whats Next? 1. Scaling up to larger networks 2. Specifications beyond local robustness 3. Most networks don t pass formal verification: need robust training 4. Look at more applications 26 / 27

26. Thank You! Questions? 27 / 27