The Challenge of Evolutionary Verification The Amir Pnueli

The Challenge of Evolutionary Verification The Amir Pnueli

The Challenge of Evolutionary Verification The Amir Pnueli Memorial Symposium NYU, 9 May 2010 Roni Rosner Intel Israel Design Center, Haifa, Israel 09-May-10 Slide 1 The Four-Color Theorem 1852: Guthrie conjectured Every planar map is four-colorable 1976: Appel & Haken proved the theorem using an assembly program on a IBM 370-168 computer 2004: Gonthier verified the proof of the theorem using the Coq proof checker 2005: Devlin [Math. Assoc. America] announced Last doubts removed about the proof of the Four Color Theorem 2006: Harrison partially verified HOL light, the logical kernel of Coq,

using HOL light itself Even for most non-typically well defined problem - math, formalization and verification are not so easily attainable 09-May-10 Slide 2 A Different Aspect of Uncertainty 1976 layers Assembly program Assembler Operating system (with VM!) Mainframe 09-May-10 2004 layers

Data: proof Application: proof-checker Compiler(s) Operating system + updates Dual-core system Network connection Slide 3 A Typical Application 2010 layers

Data Application Compiler(s) Operating system(s) Virtualization layer(s) Multi core / multi processor Heterogeneous network Dynamic aspects Runtime downloadable data / scripts Dynamic libraries Dynamic compilation Online SW updates Anti virus at the background Viruses OS patches Virtualization layer

Cloud computing The interfaces between abstraction layers as well as inside layers get more complex, dynamic and unstable more reasons for doubts!!! 09-May-10 Slide 4 Outline Motivation and conception of an evolutionary approach for verification Supporting examples Initial thoughts about potential directions 09-May-10 Slide 5

Motivation Verification task refers to a single, isolated transition Given model, system, assumptions, specification Apply an algorithmic verification process Desired correctness outcome: once proved - done forever Modern systems are of a more progressive nature Systems evolve, assumptions change Underlying models adapt, correctness criteria get refined Verification methods improve, adjust Correctness concerns are never fully satisfied Hypothesis Systems fast evolution and complexity make it increasingly inefficient / impossible to target system time-snapshots by isolated verification tasks 09-May-10 Slide 6 Proposal: Evolutionary Verification Challenge: Extend the scope of formal-methods research from

(isolated) verification tasks to the context of (evolutionary) verification process This requires the development of a formal framework that can adapt to and express the evolution of Specifications Computational/programming model Verification methods Correctness criteria and metrics Methods for handling intermediate, incorrect states and their ongoing integration into the implementation process. 09-May-10 Slide 7 Put into Historical Perspective Strongly Inspired by some of Amir Pnuelis Major Contributions Verification Task

Valid! Input Valid! Input* Adding time and state to the system and its spec Transformational System Verification Task Reactive System

Adding laziness to the verification process Verification Task Valid for P! Input P Compiler 09-May-10 Verification Process Adding time and state to the verification process??? Evolving System

Slide 8 Case for Evolution (1) - Racing Characteristics Systems are too complex to fully verify in advance Systems (at least initial) reaction/output is required earlier than full verification can complete Examples Just in time (JIT) compilation Dynamic binary optimizers (DBO) Virtualization layers 09-May-10 Slide 9 Case for Evolution (2) - Unpredictability Characteristics System behavior is changing dynamically Modes of operations / usage environments are amorphous / not known in advance

Examples WEB applications, e.g. Java scripts Viruses and anti viruses Operating systems Server networks Cloud computing 09-May-10 Slide 10 Case for Evolution (3) - Maliciousness Characteristics Optimized systems Explicit interfaces (e.g. ISA, programming model) are preserved, yet implicit assumptions of the applications are broken Knowledge of implementation details enables unexpected attacks Examples - RSA encryption Side channel attack on the Secure Socket Layer (SSL) protocol (protecting online transactions)

Exploits intimate knowledge of HW optimizations such as caches and branch prediction Exploit intimate knowledge of the algorithmic implementation of the protocol Utilize innocent OS features such time sharing to spy into the protocol Gain observability into tiny timing effects uncovering the private key 09-May-10 Slide 11 So How Evolution? All three cases (racing, unpredictability, maliciousness) have several characteristics in common Complexity Impossibility to validate in advance A sense of continuous struggle for correctness Need to tolerate intermediate failures Can incessant, lazy-verification become a more robust evolutionary model? Specification, verification are building blocks of the continuous design process

While competing for system resources, need to address How to manage the evolving specification, correctness status What to do about incorrect output? How to fix a failing system? How to improve verification over time (learn)? 09-May-10 Slide 12 Why is Evolutionary Verification an Appropriate Challenge? Interesting? subjective Difficult? necessary, not sufficient Inspired by real world problems Has the potential of expanding the scope and outreach

of formal methods, by Addressing some fundamental questions about the very nature of formal models What is a (good) specification? What defines the limits and the desired flexibilities of a formal model? Allowing for better design engineering 09-May-10 Slide 13 Partial List of Related Trends and Potential Directions Open Verification Methodology (OVM) intiative Subject/aspect oriented programming Separation of concerns Self verification Assertions Artificial intelligence methods

SHADOWS Any method of gradual verification Bounded model checking Many relevant ideas I heard in the first day of the symposium 09-May-10 Slide 14 Thank You 09-May-10 Slide 15

Recently Viewed Presentations

  • Income estimates for small-areas

    Income estimates for small-areas

    A debt of gratitude is also owed to a number at the Office for National Statistics, in particular Keith Whitfield and Philip Clarke. Finally, thanks are due to David Voas for undertaking some of the preparatory work for this project....
  • ALA Chapter Leaders Forum

    ALA Chapter Leaders Forum

    The purpose of the Washington Library Association is to promote library services, continuing education and library advocacy . on behalf of the people of Washington State. 3 Key Goals, 52 Tactics, 41 completed. 2005-2007, Mission Statement Created, 79% of initiatives...
  • Los verbos de -AR - Brooklyn High School

    Los verbos de -AR - Brooklyn High School

    Los verbos de -AR Español 1 Subject Pronouns Yo = I Nosotros = We Tú = you (informal) Vosotros = You all (informal) El = he Ellos = They Ella = she Ellas = They Usted = you (formal) Ustedes...
  • Welcome to Canyon Springs 2nd Grade Curriculum Our

    Welcome to Canyon Springs 2nd Grade Curriculum Our

    Tape Diagram. Addition & Subtraction Methods. Number Bonds. The Vertical Method will not be taught in 2. nd. grade. 18 + 22 +2-2. 18 + 2. 22 - 2. Homework is to cement skills already learned in class. Please have...
  • Fake News: a Media Literacy Workshop

    Fake News: a Media Literacy Workshop

    What is Fake News? Fake news is a type of hoax or deliberate spread of misinformation (false information), be it via the traditional print or broadcasting news media or via Internet-based social media. To qualify as fake news, a story...
  • Image credit: Victor GAD Marija Dalbello Reading Interests

    Image credit: Victor GAD Marija Dalbello Reading Interests

    16) New Age is an overall attitude and context of spirituality in response to the cultural uncertainty of our times What is "New Age" fiction Definitions _____ "New Age fiction is a meeting point of science fiction and mythical reality...
  • Working with Practices: The Practice Level Key Drivers

    Working with Practices: The Practice Level Key Drivers

    Articulate the six key drivers that provide a framework to improve ADHD care. Describe characteristics of a reliable system of ADHD care. Describe decision aids and resources to be used at point of care to support parents
  • Rootstocks - Aggie Horticulture

    Rootstocks - Aggie Horticulture

    NO2 NO2 Cl GSH GST NO2 NO2 GS HCl GST-catalyzed Conjugation of CDNB to GSH 1-chloro-2,4-dinitrobenzene Dinitrophenyl glutathione INSOLUBLE SOLUBLE Toxic Less toxic Limonoid Aglycone Limonoid Glucosides Limonoids and Flavonoids Isolation and Characterization Bioactive Compounds Flavonoids Limonoids Cell Culture Phase...