Formal VerificationSlide 2Formal ApproachVerification techniques – Criteria for classifyingPropositional logicSlide 6Inductive verificationModel-checkingFormal Verification: ComponentsSpecification LanguagesSlide 11Example: SPECIALExample: Enhanced Hierarchical Development MethodologySlide 14Levels of AbstractionHDM VerificationBoyer-Moore Theorem ProverSlide 18Gypsy verification environment (GVE)Other ExamplesSlide 21Protocol VerificationFormal VerificationLecture 11Formal VerificationFormal verification relies onDescriptions of the properties or requirementsDescriptions of systems to be analyzed, andVerification techniques showing requirements are met by system descriptionRely on underlying mathematical logic system and the proof theory of that systemFormal ApproachFormal Models use language of mathematicsSpecification languagesFor policies, models and system descriptionsWell-defined syntax and semantics – based on mathsCurrent trends - two general categoriesInductive techniquesModel checking techniquesDifferences based onIntended use, degree of automation, underlying logic systems, etc.Verification techniques – Criteria for classifyingProof-based vs model-basedProof: Formula define premises / conclusionsProof shows how to reach conclusions from premisesModel-based: Premises and conclusions have same truth tablesDegree of automationmanual or automated (degree)Propositional logicVerification techniques – Criteria for classifyingFull verification vs property verificationDoes methodology model full system?Or just prove certain key properties?Examples?Intended domain of applicationHW/SW, reactive, concurrentPredevelopment vs post developmentAs design aid or after designInductive verificationTypically more generalUses theorem proversE.g., uses predicate calculusA sequence of proof steps starting with premises of the formula and eventually reaching a conclusionMay be used To find flaws in designTo verify the properties of computer programsModel-checkingSystems modeled as state transition systemsFormula may be true in some states and false in othersFormulas may change values as systems evolveProperties are formulas in logicTruth values are dynamicShow: Model and the desired properties are semantically equivalentModel and properties express the same truth tableOften used after development is complete but before a product is released to the general marketPrimarily for reactive, concurrent systemsFormal Verification:ComponentsFormal Specification defined in unambiguous (mathematical) languageRestricted syntax, and well-defined semantics based on established mathematical conceptsExample:?Implementation LanguageGenerally somewhat constrainedFormal Semantics relating the twoMethodology to ensure implementation ensures specifications metSpecification LanguagesSpecify WHAT, not HOWValid states of systemPost-conditions of operationsNon-ProceduralTypical Examples:Propositional / Predicate LogicTemporal Logic (supports before/after conditions)Set-based models (e.g., formal Bell-LaPadula)Specification LanguagesMust support machine processingStrong typingModel input/output/errorsExample: SPECIALFirst order logic basedStrongly typedVFUN: describes variables (state)OFUN/OVFUN: describe state transitionsExample: SPECIALMODULE Bell_LaPadula_Model Give_readTypesSubject_ID: DESIGNATOR;Object_ID: DESIGNATOR;Access_Mode: {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() -> Accesses accesses: HIDDEN;INITIALLY FORALL Access a: a INSET 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_MODULEExample: Enhanced Hierarchical Development MethodologyBased on HDMA general purpose design and implementation methodologyGoal wasTo mechanize and formalize the entire development processDesign specification and verification + implementation specification and verificationProof-based methodUses Boyer-Moore Theorem ProverExample: Enhanced Hierarchical Development Methodology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 theorem-prover understood formSuccessfully used on MLS systemsFew formal policy specifications outside MLS domainLevels of AbstractionHDM VerificationBoyer-Moore Theorem ProverFully automatedNo interface for comments or directionsUser provides all the theorems, axioms, lemmata, assertionsLISP like notationVery difficult for proving complex theoremsKey ideaUsed extended propositional calculusEfficiency – to find a proof.Boyer-Moore Theorem ProverSteps:Simplify the formulaReformulate the formula with equivalent termsSubstitute equalitiesGeneralize the formula by introducing variablesEliminate irrelevant termsInduct to proveGypsy verification environment (GVE)Based on PascalFormal proof and runtime validation supportSpecifications defined on proceduresEntry conditions, Exit conditions, AssertionsProof techniques ensure exit conditions / assertions met given entry conditionsAlso run-time checkingExamples:Gypsy (in book) – uses theorem proverCLUEiffel (and derivatives) – run-time checksOther 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.Other ExamplesFormal verification of protocolsKey managementProtocol developmentVerification of librariesEntire system not verifiedBut components known okayHigh risk subsystemsProtocol VerificationGenerating protocols that meet security specificationsAssumes cryptography secureBut cryptography is not