Computer Security 463.6.1 Formal MethodsReadingOverviewIntroductionThe Limits of Formal MethodsWhat Formal Methods Can DoHow They Can HelpHistory-PastProcess of ProvingThe Orange BookTools Specific for SecurityMajor Approaches to FMVariant of Otway-Rees ProtocolAttack to the Example ProtocolA correct protocolTwo Quick Case StudiesStudy 1: Cramming AttacksTunnel as CountermeasureL3A Set-UpL3A Set-Up With ReuseMethodologySimulatorsOverview of Module InteractionSlide 24Modeling Uncovered ProblemsStudy Did Not ModelAbstractionsStudy 2: WSEmail ProtocolProof TechniqueMessage ExampleResultCase Study 3: HIPPA VerificationOur ApproachVerificationModel exampleSlide 36SummaryComputer Security463.6.1 Formal MethodsUIUC CS463 Computer Security2•J. M. Wing. A symbiotic relationship between formal methods and security. Proceedings NSF Workshop on Computer Security, Fault Tolerance, and Software Assurance: From Needs to Solution. December 1998. •Bishop, Chapter 20Reading3Overview•Types of formal methods•Subtle errors in protocols•Three illustrative case studies4Introduction•Formal method: automated technique based on mathematical logic used to analyze a property of a system•National Security Agency was the major source of funding formal methods research and development in the 70s and early 80s–Formal security models –Tools for reasoning about security–Applications of using these tools to prove systems secure•The use of Internet brings security to the attention of masses–What kind of problems can formal methods help to solve in security–What problems will formal methods never help to solve5The Limits of Formal Methods•Systems will never be 100% secure–Formal methods will not break this axiom•Assumptions about the system’s environment–Hard to state them explicitly –The system could be deployed in an environment not originally designed•For convenience or lack of an alternative–Clever intruders find out how to violate these assumptions•Security is not an either/or property–Pay more, gain more–E.g. Passwords, certificates, biometrics are measured in terms of degree of security for authentication6What Formal Methods Can Do•Delimit the system’s boundary: the system and its environment •Characterize a system’s behavior more precisely•Define the system’s desired properties precisely•Prove a system meets its specification –Tell under what circumstances a system cannot meet its specification7•These capabilities of formal methods help practitioner in two ways–Through specification, focusing on designer’s attention•What is the interface•What are the assumptions about the system•What is the system supposed to do under this condition and that condition•What are the system’s invariant properties–Through verification•Prove a system meets its security goals•Find out the weaknesses of the systemHow They Can Help8History-Past•Early formal method research funded by the National Security Agency, centered on proving systems secure–Bell-LaPadula model–Biba integrity model–Clark-Wilson model•The systems of interest to prove secure were operating systems, more specifically, kernels9Process of Proving•Process of proving entails 3 parts–Formal specification•State the property of the system •For example: *-property–Model the system so that one can formally prove the property•Model might be a semantic structure like a state machine or a syntactic structure like a logical expression–Proof•Methods–Rely on induction over traces of the state machine model–Or rely on deduction to show that an implication holds•Automatically proved by machine or require interactive guidance of human10The Orange Book•US Trusted Computer System Evaluation Criteria – The Orange Book–Produced by NCSC (National Computer Security Center) in 1985–Provide a standard metric for NCSC to compare the security of different computer systems–Guide computer system vendors in the design and development of secure systems–Provide a means for specifying security requirements in Government contracts•Levels: D, C1,C2, B1, B2, B3, A1, A2•Certified A1 means that one has formally specified the system’s security requirements, formally modeled the system, and formally proved that the model meets its specification11Tools Specific for Security•Tools specific to reason about security–Specifies an insecure state and the tool searches backwards to determine whether that state is reachable•Interrogator–Based on Prolog, exhaustive search, fully automatic•NRL Protocol Analyzer–Based on Dolev and Yao’s work on algebraic term rewriting model for two-party cryptographic protocols–Less automatic•BAN logic – Logic of Authentication –Reason in terms of belief logic •Accumulates belief during the run of the protocol12•Model checking– Example: FDR (NS counter-example)•Theorem proving–Example: Isabelle•Software specification–Example: ZMajor Approaches to FM13Variant of Otway-Rees ProtocolA and B share keys Ka and Kb respectively with S1. A ! B: Na, A, B, {| Na, A, B|}Ka2. B ! S: Na, A, B, {| Na, A, B|}Ka, Nb, {| Na, A, B|}Kb3. S ! B: Na, {| Na, Kab |}Ka, {| Nb, Kab |}Kb4. B ! A: Na , {| Na, Kab |}Ka14Attack to the Example Protocol•An attack on the protocol1. A ! B £ : Na, A, B, {| Na, A, B|}Ka1’. C ! A : Nc, C, A, {| Nc, C, A|}Kc2’. A ! S £ : Nc, C, A, {| Nc, C, A|}Kc ,Na’, {| Nc, C, A|}Ka 2’’. C(A) ! S : Nc, C, A, {| Nc, C, A|}Kc ,Na, {| Nc, C, A|} Ka 3’. S ! A £ : Nc, {| Nc, Kca |}Kc, {| Na, Kca |}Ka4. C(B) ! A : Na , {| Na, Kca |}Ka Replacing Na’ by A’s original nonce Na eventually causes A to accept key Kca as a key shared with B15A correct protocol1. A ! B: Na, A, B, {| Na, A, B|}Ka2. B ! S: Na, A, B, {| Na, A, B|}Ka, {| Na, Nb, A, B|}Kb3. S ! B: Na, {| Na, Kab |}Ka, {| Nb, Kab |}Kb4. B ! A: Na , {| Na, Kab |}Ka16Two Quick Case Studies•Formal Simulation of L3A–Maude•Formal Verification of On-Demand Attachments–Proverif and TulaFale•Formal Analysis of HIPPA–Privacy APIs and SPIN17Study 1: Cramming AttacksClientServerAccountingSystemAttackerE2E SecurityTunnelNetworkAccessServer(NAS)NAS SecurityTunnelUnauthenticatedIngressGoodloe, Gunter, Stehr 0518Tunnel as CountermeasureChallenge: Coordinate the creation of the tunnels19L3A Set-UpClient NAS ServerReq(cred)Ack(cred)Fin SPD CS:(CN) SPD CS:(CN) SPD SC:(SN) SPD:SC:(SN)20L3A Set-Up With ReuseClient
View Full Document
Unlocking...