CS18000 Programming I 11 1 2010 CS52600 Information Security Formal Verification 1 November 2010 Prof Chris Clifton Formal Verification Components Formal Specification defined in unambiguous mathematical language Example security policy models Implementation Language Generally somewhat constrained Formal Semantics relating the two Methodology to ensure implementation ensures specifications met CS526 Spring 2003 2010 Chris Clifton 2 1 CS18000 Programming I 11 1 2010 Specification Languages Specify WHAT not HOW Valid states of system Postconditions of operations Non Procedural Typical Examples Propositional Predicate Logic see Chapter 34 Temporal Logic supports before after conditions Set based models e g formal Bell LaPadula model of 5 2 3 CS526 Spring 2003 3 Specification Languages Must support machine processing Strong typing Model input output errors Example SPECIAL First order logic base Strongly typed VFUN describes variables state OFUN describe state transitions CS526 Spring 2003 2010 Chris Clifton 4 2 CS18000 Programming I 11 1 2010 Example SPECIAL if r 6 then 6 r v i v else if o root o and parent o root o and parent o b s1 w or parent o root o and canallow s1 o v or o root o and canallow s1 root o v then 6 r v y b m m s2 o r f h else 6 r v n v MODULE Bell LaPadula Model Give read Types Subject ID DESIGNATOR Object ID DESIGNATOR Access Model READ APPEND WRITE Access STRUCT OF Subject ID subject Object ID object Access Mode mode Functions VFUN active Object ID object BOOLEAN active HIDDEN INITIALLY TRUE VFUN access matrix Access accesses HIDDEN INITIALLY FORALL Access a a INSERT accesses active a object OFUN give access Subject ID giver Access access ASSERTIONS active access object TRUE EFFECTS access matrix access matrix UNION access END MODULE CS526 Spring 2003 5 Verification Methodologies Proof based vs model based Proof Formula define premises conclusions Proof shows how to reach conclusions from premises Model based Premises and conclusions have compatible truth tables Full vs property verification Does methodology model full system Or just prove certain key properties Automation may be manual or have tool support CS526 Spring 2003 2010 Chris Clifton 6 3 CS18000 Programming I 11 1 2010 Example Enhanced Hierarchical Development Methodology Proof based method Uses Boyer Moore Theorem Prover Hierarchical approach Abstract Machines defined at each level specification written in SPECIAL Mapping Specifications define functionality in terms of machines at higher layers Consistency Checker validates mappings match Compiler that maps a program into a theoremprover understood form Successfully used on MLS systems Few formal policy specifications outside MLS domain CS526 Spring 2003 7 Alternate Approach Combine Specifications and Language Specifications defined on procedures Entry conditions Exit conditions Assertions Proof techniques ensure exit conditions assertions met given entry conditions Also run time checking Examples Gypsy in book uses theorem prover CLU Eiffel and derivatives run time checks CS526 Spring 2003 2010 Chris Clifton 8 4 CS18000 Programming I 11 1 2010 Other Examples Prototype Verification System PVS Based on EHDM Interactive theorem prover Symbolic Model Verifier Temporal logic based Notion of path program represented as tree Statements that condition must hold at a future state all future states all states on one path etc CS526 Spring 2003 9 Is this Real Formal verification of protocols Key management Protocol development Verification of libraries Entire system not verified But components known okay High risk subsystems CS526 Spring 2003 2010 Chris Clifton 10 5 CS18000 Programming I 11 1 2010 CS52600 Information Security Formal Evaluation 1 November 2010 Prof Chris Clifton What is Formal Evaluation Method to achieve Trust Not a guarantee of security Evaluation methodology includes Security requirements Assurance requirements showing how to establish security requirements met Procedures to demonstrate system meets requirements Metrics for results Examples TCSEC Orange Book ITSEC CC CS526 Spring 2003 2010 Chris Clifton 14 6 CS18000 Programming I 11 1 2010 Formal Evaluation Why Organizations require assurance Defense Telephone Utilities Mission Critical systems Formal verification of entire systems not feasible Instead organizations develop formal evaluation methodologies Products passing evaluation are trusted Required to do business with the organization CS526 Spring 2003 15 TCSEC The Original Trusted Computer System Evaluation Criteria U S Government security evaluation criteria Used for evaluating commercial products Policy model based on Bell LaPadula Enforcement Reference Validation Mechanism Every reference checked by compact analyzable body of code Emphasis on Confidentiality Metric Seven trust levels D C1 C2 B1 B2 B3 A1 D is tried but failed CS526 Spring 2003 2010 Chris Clifton 16 7 CS18000 Programming I 11 1 2010 TCSEC Class Assurances C1 Discretionary Protection Identification Authentication Discretionary access control C2 Controlled Access Protection Object reuse and auditing B1 Labeled security protection Mandatory access control on limited set of objects Informal model of the security policy CS526 Spring 2003 17 TCSEC Class Assurances continued B2 Structured Protections Trusted path for login Principle of Least Privilege Formal model of Security Policy Covert channel analysis Configuration management B3 Security Domains Full reference validation mechanism Constraints on code development process Documentation testing requirements A1 Verified Protection Formal methods for analysis verification Trusted distribution CS526 Spring 2003 2010 Chris Clifton 18 8 CS18000 Programming I 11 1 2010 How is Evaluation Done Government sponsored independent evaluators Application Determine if government cares Preliminary Technical Review Discussion of process schedules Development Process Technical Content Requirements Evaluation Phase CS526 Spring 2003 19 TCSEC Evaluation Phase Three phases Design analysis Review of design based on documentation Test analysis Final Review Trained independent evaluation Results presented to Technical Review Board Must approve before next phase starts Ratings Maintenance Program Determines when updates trigger new evaluation CS526 Spring 2003 2010 Chris Clifton 20 9 CS18000 Programming I 11 1 2010 TCSEC Problems Based heavily on confidentiality Tied security and functionality Base TCSEC geared to operating systems TNI Trusted