Title of Presentation

Title of Presentation

Logic-based Modeling and Analysis Tools from Microsoft Research Nikolaj Bjrner Microsoft Research HIPERFIT Workshop May 25 - 2011 FSE & Agenda Research in Software Engineering - an overview and three (HIPERFIT fit?) projects Z3:

An efficient SMT solver FORMULA: Formal Modeling using Logic and Analysis Other FITs from Microsoft (Research) F#: async, quotations, and metrics. Accelerator (data-parallel library). Unit testing with Pex/Moles Parallels library, concurrent revisions. HPC/Technical Computing. Engineering Research In Software

Tools Try some tools online: http://rise4fun.com RiSE EcoSystem Maintainability Benefits R e s e a r c h P

r o j e c t s Reliability Security/Privacy Performance - Env construction (.NET moles) - Security testing (bin: Sage) - Code contracts (.Net)

- Security audits (C: havoc) - Perf analysis (bin: speed) - Conc. testing(bin: Chess, ..) - Sec analysis (JS: gatekeeper) - Race detectors () - Semantic diff - E2E security verification (Fine) - Model-driven eng. (Formula) - Verifying System Pgms (VCC) - Verifying OO Pgms (Spec#, Daphne) - Synthesis of end user pgms (ITI Sans-script) SE Dev.-Analysis - Prediction (CRANE)

- Assessment (TDD, Distr. Dev, ..) - Process optim. (HR network ana.) Verification SMT Platform Solver (Boogie) (Z3) Logic Predictability - Distributed authorization (DKAL) - Unit testing (.NET pex) Core

Competencies Analyzability Energy Modeling, synth., Verif. Code Analysis Root Technologies Programmability/Extensability Automata

Software Development Datamart (CodeMine) Statistics Runtimes, Optimization - Tracing JITs (.NET: Spur) - Bowser Extensions (C3) - Benchmarks (JS, HTML) - Download optim (JS: Dolotto) - Mem Manager (bin: DieHard) - Malware detector (bin: Noozle) - Adaptive QoS comp (bin:Green) - Pgm. Mod (.NET: TPL, Version) - Mem.Mod (Travers,..) Web-Client Compiler/Runtime Platform

Infrastructure (C3) (.NET:CCI, Spur, ER) Semantics Type Systems Tools using Z3 Property Driven Execution Guided Program Verification

Model Based OverApproximation Testing Analysis BEK Auditing HAVOC SLAyer

Type Safety UnderApproximation SAGE Synthesis SAGE by numbers Slide shamelessly stolen and adapted from [Patrice Godefroid, ISSTA 2010] 100+ CPU-years - largest dedicated fuzz lab in the world 100s apps - fuzzed using SAGE 100s previously unknown bugs found 1,000,000,000+ computers updated with bug fixes

Millions of $ saved for Users and Microsoft 10s of related tools (incl. Pex), 100s DART citations Formal Modeling using Logic and Analysis Ethan Jackson, Nikolaj Bjrner and Wolfram Schulte Research in Software Engineering (RiSE), Microsoft Research Dirk Seifert, Markus Dahlweid and Thomas Santen, European Microsoft Innovation Center (EMIC), Aachen, Germany Overview Introduction to the FORMULA formal specification language An example using FORMULA for platform mappings

What is FORMULA? Provides general language capturing model-based abstractions Supports automated model synthesis What is FORMULA? Provides general language capturing model-based abstractions Core based on CLP with negation. Uniform Regular type system (ICLP 2011) Specs composed as modules. Abstraction boundaries managed by module system. Supports automated model synthesis What is FORMULA? Provides general language capturing model-based abstractions

Core based on CLP with negation. Uniform Regular type system (ICLP 2011) Specs composed as modules. Abstraction boundaries managed by module system. Supports automated model synthesis Formal descriptions of design spaces and model checking problems Solves open CLP systems Find me the facts such that my query holds. The FORMULA Tool An example FORMULA

The Software Components (I) For simplicity, assume a software component is just a task. Two tasks can be in conflict, meaning they should not execute on the same device. SCM Map PM T1 T3 T2

The Software Components (II) SCM Map PM The Platform (I) Nodes are connected by channels with communication capacities. No node can support more than two incoming and outgoing channels. Capacities must be balanced on node with incoming and outgoing channels. Map PM

In-degree = 0 Out-degree = 1 In capacity = 0 Out capacity = 8 D1 SCM In-degree = 1 Out-degree = 0 In capacity = 4 Out capacity = 0 D4 4

8 D2 In-degree = 1 Out-degree = 2 In capacity = 8 Out capacity = 4+4 4 D3 The Platform (II) SCM Map

PM The Mapping (I) Tasks should be place on nodes so all conflict constraints are respected. SCM Map T2 PM D4 4 D1

T1 8 D2 4 D3 T3 The Mapping (II) SCM Map PM

A number of constraint problems are in this specification, including: A coloring problem, A forbidden-subgraph problem Linear arithmetic problem Similar process to add new architectural facets onto this structure Solve in Any Direction The user constructs a partial model to represent the degrees of freedom in the problem. Degrees of freedom can be anywhere. Design Space Exploration Given a spec and a partial model, then symbolic execution constructs a formula representing the design space. Formula Specification

Symbolic Execution Add symmetry breaking Encode solution region Z3 Solver Reconstruct FORMULA model Cardinality bounds on record instances SMT Formula

Try something new Pick next region A Verifying ML Compiler Karthik Bhargavan Juan Chen Cedric Fournet Pierre-Yves Strub Nikhil Swamy Jean Yang F* type system: Dependently typed Core ML, with higher kinding, and affine types F* combines several projects at MSR

Fine: Security-oriented F# subset (ESOP 10) DCIL: Dependently typed .NET bytecode (PLDI 10) Ibex/RePriv: Dependently typed web browser extensions (2 x Oakland 11) F7: Refinement types for crypto protocols (CSF08, POPL 10)

FX: Modular verification of stateful code (PLPV 11) F* Source: core-ML with dependent refinement types x:int -> {y:int | x > y} F* source Preserve types in .NET class C *> Interop with C#, VB.NET, F#, rDCIL

Run on Azure, Windows Phone 7 Z3 C#, F#, DCIL Type-Checker DCIL .NET Virtual Machine Z3 Type-checker + Compiler

Java Script Web demo: rise4fun.com/fstar WEB BROWSER EXTENSION SECURITY 1. 1/3rd of Firefox users run extensions (~34 million users) 2. Popular Chrome extensions have thousands of users mailto:[email protected] Ch an

ge m ailt o: lin ks to evil.com? Change links https://mail.google.com/mail/? [email protected]&cc=&su=&body =&fs=1 Google Dictionary Service

evil.com Se nd my e ma il Se cte e l e t s

o s nd ev il to d r o dw .co m? le

g o Go 60% 30% (of 1,137) (of 1,137) have have access access to history, to your storage, data on all and websites

the Web IBEX: Formal Basis for Browser Extension Security Secure-by-construction extensions Expressive, fine grained policies Tools to understand policies Cross-platform deployment Extension policy Extension in F*

Developers ML/F# dialect with a Write extensions and type system for policies in F* program verification Use tools to ensure extension conforms 1. Datalog-style authorization logic for F* to policy Curator

Policy Visualizer writing policies Compiler & Verifier Secure DOM API Uses tools to ensure code matches policy n 2. Secure DOM API o Uses visualizer to help

ti 3. Semantics and type la soundnesspolicy not violated o understand policy i V 5. Visualize fine-grained access-control policies on Users examples Trust curated gallery type-preserving compiler to .NET

C3 new compilerextension to JavaScript Install approved extensions 4. Cross-platform deployment; retrofitted security Question: What is the security policy? Bookmarks my friends Websites Can Read Names Jean Yang Can Read Websites

(and ability to bookmarkelided) http://people.csail.mit.edu/jeanyang Principle of Least Authority Basic Extension: read text in Secure DOM API DOM predicates and permissions

Policy language Extension code type elt Native DOM elements, abstract to F* val getInnerText : elt -> string val getTagName : elt -> string Defined in

.NET/JavaScript with this type A Refined API for the DOM type elt val getInnerText : { e:elt | CanRead e} -> string val getTagName : elt -> string Precondition; DOM permission A Refined API for the

DOM assumption in the model type elt can read tag names and attribute names val getInnerText : { e:elt | CanRead e} -> string Precondition; DOM permission val getTagName : e:elt -> { s:string | EltTagName e s}

Postcondition; DOM predicate Refined DOM API type elt assume (e:elt) . EltTagName e e:elt) . EltTagName e "head" CanRead e val getInnerText : { e:elt | CanRead e} -> string Re q

uir es val getTagName : e:elt -> { s:string | EltTagName e s} s F* + Z3 check and post-conditions statically repreu s n let read elt = E if getTagName elt = "head" then getInnerText elt else

"not Extension source code Extension in F* Extension policy Extension in F* Extension policy Extension in F* Extension policy Extension in F* Extension policy F* Compiler & Verifier

Secure DOM API 1. Single DOM API 2. No code audit 3. No security exceptions (robust) and no runtime overhead (fast) C3 research.microsoft.com/fstar

Recently Viewed Presentations

  • Exposure - BA English Revision

    Exposure - BA English Revision

    'Compare the way poets present power / conflict in [named poem] and one other from the anthology' Know the key poems well, and find basic links between them. Know the key poems in detail, with some analysis of language and...
  • Equilibrium, Acids & Bases

    Equilibrium, Acids & Bases

    ICE Charts and Equilibrium Calculations Example #4: Using the Approximation Rule Calculate the concentration of gases produced when 0.100 mol/L COCl. 2(g) decomposes into carbon monoxide and chlorine gas. The K c. for this reaction is 2.2 X 10-10.
  • ESO 208A: Computational Methods in Engineering Lecture 1

    ESO 208A: Computational Methods in Engineering Lecture 1

    Active Richardson's Extrapolation with Euler Forward: 4th order method start-up. We will now apply the Euler Forward and Richardson's extrapolation with the extrapolated initial value at . t = 0.4 and go up to . t = 0.8
  • Who am I?  Biomedical Engineering Ph.D. Student  Means:

    Who am I? Biomedical Engineering Ph.D. Student Means:

    59.4µm/hour growth rate. Relative to: Your hair grows about 417µm per day! Scientific notation? 4x magnification. Confusing math equation. Basically…4x of your normal eyesight . 250mm from your eye = focus distance. Cells! Can you guess what kind of cells?...
  • Outline for FOSAMAX PLUS Slide Set

    Outline for FOSAMAX PLUS Slide Set

    Simon R. Lost interest. Warrell. Move in with daughter in Wales. Tobert. Lewis. Brown M. No. of falls in control period _ There are no subjects for sub.no's 41,45,46,74 and 76. Only diaries for subjects 77,78,80 and 82. ill-health. moved...
  • SANDI FAST - Riverside County Office of Education

    SANDI FAST - Riverside County Office of Education

    What we found is we had no assment that students could access, that was fair and reliable, linked to CA standards, so we began ourselves to put those systems in place. RCOe vehicle is PLC's - tools we use =...
  • INTERNET SAFETY FOR EVERYONE - media.gcflearnfree.org

    INTERNET SAFETY FOR EVERYONE - media.gcflearnfree.org

    Identity theft and invasions of privacy can have very real consequences. Taking certain precautions and adopting safe habits can go a long way toward protecting you from personal harm. Guard your personal information.
  • Introducing ART UCSFs Application, Review and Tracking (ART)

    Introducing ART UCSFs Application, Review and Tracking (ART)

    Applicants' View / Confirmation Email . Dear Nick, Thank you for completing your application to the CTSI Education program. Here is a link to your personalized portal where we have posted your submitted application and will post other relevant program...