際際滷

際際滷Share a Scribd company logo

Ofer rivlin BGU - department seminar

Ofer Rivlin, CISSP
Ofer Rivlin, CISSP

A department seminar I gave at the department of Software, Information Systems Engineering and Cyber, Ben-Gurion University. Agenda: - Ways for the Industry to consume an academic research - Example: - provable software & security - Analysis tools demos - Avispa & Tamarin Prover - Advanced attacks/analysis/next steps

1 of 56
Download to read offline
PROVABLE SECURITY FORMAL PROOFS OF CRYPTOGRAPHIC PROTOCOLS 1 Ofer Rivlin Security Technology Research Lead
Security Technology Research Leader 10 years of cybersecurity research and security-architecture 10 years of software development and software architecture Startups in Canada and Israel, SAP, General-Motors and CyberArk Enterprise solutions, cloud, connected vehicles cryptography and application security Formal Methods for provable software Games Artificial-Intelligence OFER RIVLIN 2
Ways for the Industry to consume an academic research Example: provable software & security Analysis tools demos Avispa & Tamarin Prover Advanced attacks/analysis/next steps Summary AGENDA 3
4 WAYS FOR THE INDUSTRY TO CONSUME AN ACADEMIC RESEARCH
5
6
7 IBM Research Microsoft ResearchMicrosoft Research
Stay relevant catch up with new technologies technology, especially in the cybersecurity domain advances at a huge speed plan the next generation products be attractive to excellent tech employees SMALL - MEDIUM COMPANIES, ESPECIALLY VETERAN COMPANIES 8
9
Target: knowledge on new technologies accessible and consumable Choose technology as research target Great exposure to all relevant new technologies Theoretical possibilities for that technology in the target domain / use cases Open new opportunities/close domains (i.e. privacy, connected vehicles, etc.) improve /secure our products and processes (formal proving) Learn, assess and POC Push the technology into the R&D Knowledge sharing with R&D publications (internal and external) lectures, training, workshops innovation TECHNOLOGY AS A RESEARCH TARGET FOR THE R&D 10
Zero Knowledge Proof GDPR and the latest emphasis on privacy Rise of Blockchain may open up new markets identification while maintaining privacy i.e. connected vehicles protocols, financial world Formal Methods and Provers leading cloud vendors use Formal Reasoning to increase their cloud security soundness enables proving security soundness in the comming complex security systems Blockchain A disruption technology in the domain of trust Machine Learning insights form big data in logs and by usage EXAMPLES OF A FEW OF MY RESEARCH SUBJECT TARGETS 11
Technology company Internal research organization collaboration with academy and private research companies like Fraunhofer industry individuals join academic projects (i.e. NModel, DEPLOY, etc.) Academic researchers researchers initiate research on industry challenges work part-time in a technology company INJECT ACADEMIC KNOWLEDGE INTO THE INDUSTRY 12
VANET/V2X REVOCATION PROTOCOL 13
Ofer rivlin BGU - department seminar
COOPERATIVE INTELLIGENT TRANSPORTATION SYSTEMS (CITS) detect insider attacks based on attacker behavior V2X Revocation Protocol
ORDER FOR SELF REVOCATION REQUEST & RESPONSE - R-TOKEN
R-TOKEN SCHEME
18
MODEL BASED TESTING 19
20
21
22
forward chaining / traversing properties like safety and liveness safety analysis unsafe (forbidden) states liveness analysis dead states from which goals cannot be reached deadlocked state - no outgoing transitions livelocks - loop that never threach e end-state) FUNCTIONAL MBT 23
24 PROVABLE SOFTWARE & SECURITY
25 THE CHALLENGE
26 Step Alice-Bob Notation Description 1 A -> B: {Na.A}_Kb A sends a message to B with a Nonce Na + its identity. The message is encrypted using Kb which is Bs public key 2 A <- B: {Na.Nb}_Ka B returns a message to A with Na and with Nb - a new nonce by B. The message is encrypted using Ka which is As public key 3 A -> B: {Nb}_Kb A proves its identity by returning Nb to B. The message is encrypted using Kb which is Bs public key A mutual authentication protocol The nonce data are secrets that are shared between A & B IS THIS PROTOCOL SAFE?
the Needham-Schroeder (Roger Needham & Michael Schroeder) Public Key protocol (1978) Mutual authentication with public keys (using a trusted key server) MITM attack published by Gavin Lowe, using a model-checker in 1995 (Link), 17 years later! THE NEEDHAM SCHROEDER PUBLIC KEY PROTOCOL 27
28
30 Roger Needham: Cryptography protocols are three line programs that people still manage to get wrong
EXAMPLE OF PROTOCOLS WE DESIGN 31
32 FORMAL PROVING MACHINE CHECKABLE CRYPTOGRAPHIC PROOFS
33 THE PROCESS Define the systems specs using a modeling language (Formal- mathematical syntax) Define a set of theorems about the behavior of a system
34
35 Dr. Strange: I went forward in time to view alternate futures. To see all the possible outcomes of the coming conflict. Peter Quill: How many did you see? Dr. Strange: Fourteen million six hundred and five. Tony Stark: How many did we win? Dr. Strange: ...One.
Coverage: exhaustive exploration of all possible behaviors Verify each behavior against the required theorems through mathematical proofs Can verify systems that are not finite space, using abstraction Provide a counter example, i.e. a Fault Trace MODEL CHECKER GOALS 36
Assumption: The intruder is an Insider! Intruder has full control over the network Intruder can play role(s) of (honest/normal) principals Knows all the public data of the network Possible actions: Start any number of parallel protocol sessions Intercept any message Generate new messages, using observed data and initial knowledge (e.g. public keys) DOLEV-YAO INTRUDER MODEL 37
Assumption: the cryptography is secure! Intruder cannot break cryptography Intruder cannot encrypt/decrypt messages if s/he doesn't have the key Intruder cannot guess a secret key or a nonce * we assume the cryptography, random, etc. are secure DOLEV-YAO INTRUDER MODEL 38
39 The adversary can use the following inference rules on the state: The set of the adversarys knowledge is K and contains facts of the form K(t) state fact state fact action fact
40 TAMARIN PROVER DEMO
Backwards chaining / reasoning / traversing advantages when the model of the system has states with more than one successor models may have infinitely many trajectories - forward traversing would be infeasible exhaustive graph-traversal often subject to the state-explosion problem. Temporal logic allows reasoning about reactive systems The unpredictability of the environment appears as branching on time state can have more than one possible future Counterexamples model checking often providing a counterexample of a case where the program does not meet the specification TAMARIN-PROVER 41
Term rewriting repeated application of substitution rules example uses: symbolic computation, program analysis and program transformation Constraint (conditional) rewrite rules TAMARIN-PROVER 42 This image cannot currently be displayed. = {X senc(M,K)} t = sdec(X,K) = sdec(senc(M,K),K)t This image cannot currently be displayed. Subtitution Term apply the subtitution:
43 state fact state fact action fact include the reason information traces of events consist of sequences of such lables
44 role name step index s' = s+1 agent name thread identifier label 'a' is the 'action fact' X = X T(X) - signature X - terms
45 NSPK Split a message sequence into roles Generate longterm keys and public keys For each role R there must be an initialization rule which is instantiated with a name A and a thread identifier id
46 Role specification rules
DEMO 48
49 ADVANCED ATTACKS/ANALYSIS
Model Learning: (active automata learning or protocol state fuzzing) building finite-state models from observed inputoutput data on implementations An example Java Secure Socket Extension: a model was learned for Java version 1.8.0.25. Found out that the model contained two parallel paths of application data transitions: a TLS protocol run + another unexpected run Possible attack: the client and server would think they are talking on a secure connection, where in reality they are talking on an open connection (A fix was released as part of a critical security update) MODEL LEARNING 50
POSSIBLE CONNECTIONS BETWEEN MODEL LEARNING & MODEL CHECKING 51
52 SECURITY ANALYSIS OF LEARNED MODEL Model Learning
53 COMPARE LEARNED MODEL TO SPECS MODEL conformance testing tool (CT) conformance testing (Provable Software - mbt)
Learned FSM for Win8 TCP Client-Server Computed by a model checker Red transition = non-conformance to the RFC In a {Close + RCV call pending} state, can generate a RST instead of a Fin even in cases where there is no data to be received Models composition enable analysis between different components (i.e. Win client with Linux Server, etc.) EXAMPLE: TCP ON WIN8 54
56 SUMMARY
We reviewed a few examples of how academic research knowledge can advance the industry and help in solving complex problems Ways of inserting knowledge from the academia into the industry Academic researchers identify some challenges and initiate research to help solving them Academic researchers work partly in companies and startups collaboration To succeed in pushing academic knowledge into the industry simplification go from generalization to specific implementations SUMMARY 57
THANK YOU! Ofer Rivlin ofer.rivlin@cyberark.com https://www.linkedin.com/in/ofer-rivlin/ Twitter: @0xriv3r 58
Fiteru-Brotean, Janssen, Vaandrager: Combining model learning and model checking to analyze TCP implementations (2016). Springer {J.Whitefield, Liqun.Chen, S.Schneider, H.Treharne, S.Wesemeyer}@surrey.ac.uk: "Formal Analysis of V2X Revocation Protocols" https://pdfs.semanticscholar.org/6658/591533a5a41d88af1bbb112591645c0f61e0.pdf https://tools.ietf.org/html/rfc793 https://www.kb.cert.org/vuls/id/612636 http://people.irisa.fr/Thomas.Genet/span/ https://tamarin-prover.github.io REFERENCES 59

More Related Content

Ofer rivlin BGU - department seminar

  • 1. PROVABLE SECURITY FORMAL PROOFS OF CRYPTOGRAPHIC PROTOCOLS 1 Ofer Rivlin Security Technology Research Lead
  • 2. Security Technology Research Leader 10 years of cybersecurity research and security-architecture 10 years of software development and software architecture Startups in Canada and Israel, SAP, General-Motors and CyberArk Enterprise solutions, cloud, connected vehicles cryptography and application security Formal Methods for provable software Games Artificial-Intelligence OFER RIVLIN 2
  • 3. Ways for the Industry to consume an academic research Example: provable software & security Analysis tools demos Avispa & Tamarin Prover Advanced attacks/analysis/next steps Summary AGENDA 3
  • 4. 4 WAYS FOR THE INDUSTRY TO CONSUME AN ACADEMIC RESEARCH
  • 5. 5
  • 6. 6
  • 8. Stay relevant catch up with new technologies technology, especially in the cybersecurity domain advances at a huge speed plan the next generation products be attractive to excellent tech employees SMALL - MEDIUM COMPANIES, ESPECIALLY VETERAN COMPANIES 8
  • 9. 9
  • 10. Target: knowledge on new technologies accessible and consumable Choose technology as research target Great exposure to all relevant new technologies Theoretical possibilities for that technology in the target domain / use cases Open new opportunities/close domains (i.e. privacy, connected vehicles, etc.) improve /secure our products and processes (formal proving) Learn, assess and POC Push the technology into the R&D Knowledge sharing with R&D publications (internal and external) lectures, training, workshops innovation TECHNOLOGY AS A RESEARCH TARGET FOR THE R&D 10
  • 11. Zero Knowledge Proof GDPR and the latest emphasis on privacy Rise of Blockchain may open up new markets identification while maintaining privacy i.e. connected vehicles protocols, financial world Formal Methods and Provers leading cloud vendors use Formal Reasoning to increase their cloud security soundness enables proving security soundness in the comming complex security systems Blockchain A disruption technology in the domain of trust Machine Learning insights form big data in logs and by usage EXAMPLES OF A FEW OF MY RESEARCH SUBJECT TARGETS 11
  • 12. Technology company Internal research organization collaboration with academy and private research companies like Fraunhofer industry individuals join academic projects (i.e. NModel, DEPLOY, etc.) Academic researchers researchers initiate research on industry challenges work part-time in a technology company INJECT ACADEMIC KNOWLEDGE INTO THE INDUSTRY 12
  • 15. COOPERATIVE INTELLIGENT TRANSPORTATION SYSTEMS (CITS) detect insider attacks based on attacker behavior V2X Revocation Protocol
  • 16. ORDER FOR SELF REVOCATION REQUEST & RESPONSE - R-TOKEN
  • 18. 18
  • 20. 20
  • 21. 21
  • 22. 22
  • 23. forward chaining / traversing properties like safety and liveness safety analysis unsafe (forbidden) states liveness analysis dead states from which goals cannot be reached deadlocked state - no outgoing transitions livelocks - loop that never threach e end-state) FUNCTIONAL MBT 23
  • 26. 26 Step Alice-Bob Notation Description 1 A -> B: {Na.A}_Kb A sends a message to B with a Nonce Na + its identity. The message is encrypted using Kb which is Bs public key 2 A <- B: {Na.Nb}_Ka B returns a message to A with Na and with Nb - a new nonce by B. The message is encrypted using Ka which is As public key 3 A -> B: {Nb}_Kb A proves its identity by returning Nb to B. The message is encrypted using Kb which is Bs public key A mutual authentication protocol The nonce data are secrets that are shared between A & B IS THIS PROTOCOL SAFE?
  • 27. the Needham-Schroeder (Roger Needham & Michael Schroeder) Public Key protocol (1978) Mutual authentication with public keys (using a trusted key server) MITM attack published by Gavin Lowe, using a model-checker in 1995 (Link), 17 years later! THE NEEDHAM SCHROEDER PUBLIC KEY PROTOCOL 27
  • 28. 28
  • 29. 30 Roger Needham: Cryptography protocols are three line programs that people still manage to get wrong
  • 30. EXAMPLE OF PROTOCOLS WE DESIGN 31
  • 32. 33 THE PROCESS Define the systems specs using a modeling language (Formal- mathematical syntax) Define a set of theorems about the behavior of a system
  • 33. 34
  • 34. 35 Dr. Strange: I went forward in time to view alternate futures. To see all the possible outcomes of the coming conflict. Peter Quill: How many did you see? Dr. Strange: Fourteen million six hundred and five. Tony Stark: How many did we win? Dr. Strange: ...One.
  • 35. Coverage: exhaustive exploration of all possible behaviors Verify each behavior against the required theorems through mathematical proofs Can verify systems that are not finite space, using abstraction Provide a counter example, i.e. a Fault Trace MODEL CHECKER GOALS 36
  • 36. Assumption: The intruder is an Insider! Intruder has full control over the network Intruder can play role(s) of (honest/normal) principals Knows all the public data of the network Possible actions: Start any number of parallel protocol sessions Intercept any message Generate new messages, using observed data and initial knowledge (e.g. public keys) DOLEV-YAO INTRUDER MODEL 37
  • 37. Assumption: the cryptography is secure! Intruder cannot break cryptography Intruder cannot encrypt/decrypt messages if s/he doesn't have the key Intruder cannot guess a secret key or a nonce * we assume the cryptography, random, etc. are secure DOLEV-YAO INTRUDER MODEL 38
  • 38. 39 The adversary can use the following inference rules on the state: The set of the adversarys knowledge is K and contains facts of the form K(t) state fact state fact action fact
  • 40. Backwards chaining / reasoning / traversing advantages when the model of the system has states with more than one successor models may have infinitely many trajectories - forward traversing would be infeasible exhaustive graph-traversal often subject to the state-explosion problem. Temporal logic allows reasoning about reactive systems The unpredictability of the environment appears as branching on time state can have more than one possible future Counterexamples model checking often providing a counterexample of a case where the program does not meet the specification TAMARIN-PROVER 41
  • 41. Term rewriting repeated application of substitution rules example uses: symbolic computation, program analysis and program transformation Constraint (conditional) rewrite rules TAMARIN-PROVER 42 This image cannot currently be displayed. = {X senc(M,K)} t = sdec(X,K) = sdec(senc(M,K),K)t This image cannot currently be displayed. Subtitution Term apply the subtitution:
  • 42. 43 state fact state fact action fact include the reason information traces of events consist of sequences of such lables
  • 43. 44 role name step index s' = s+1 agent name thread identifier label 'a' is the 'action fact' X = X T(X) - signature X - terms
  • 44. 45 NSPK Split a message sequence into roles Generate longterm keys and public keys For each role R there must be an initialization rule which is instantiated with a name A and a thread identifier id
  • 48. Model Learning: (active automata learning or protocol state fuzzing) building finite-state models from observed inputoutput data on implementations An example Java Secure Socket Extension: a model was learned for Java version 1.8.0.25. Found out that the model contained two parallel paths of application data transitions: a TLS protocol run + another unexpected run Possible attack: the client and server would think they are talking on a secure connection, where in reality they are talking on an open connection (A fix was released as part of a critical security update) MODEL LEARNING 50
  • 50. 52 SECURITY ANALYSIS OF LEARNED MODEL Model Learning
  • 51. 53 COMPARE LEARNED MODEL TO SPECS MODEL conformance testing tool (CT) conformance testing (Provable Software - mbt)
  • 52. Learned FSM for Win8 TCP Client-Server Computed by a model checker Red transition = non-conformance to the RFC In a {Close + RCV call pending} state, can generate a RST instead of a Fin even in cases where there is no data to be received Models composition enable analysis between different components (i.e. Win client with Linux Server, etc.) EXAMPLE: TCP ON WIN8 54
  • 54. We reviewed a few examples of how academic research knowledge can advance the industry and help in solving complex problems Ways of inserting knowledge from the academia into the industry Academic researchers identify some challenges and initiate research to help solving them Academic researchers work partly in companies and startups collaboration To succeed in pushing academic knowledge into the industry simplification go from generalization to specific implementations SUMMARY 57
  • 56. Fiteru-Brotean, Janssen, Vaandrager: Combining model learning and model checking to analyze TCP implementations (2016). Springer {J.Whitefield, Liqun.Chen, S.Schneider, H.Treharne, S.Wesemeyer}@surrey.ac.uk: "Formal Analysis of V2X Revocation Protocols" https://pdfs.semanticscholar.org/6658/591533a5a41d88af1bbb112591645c0f61e0.pdf https://tools.ietf.org/html/rfc793 https://www.kb.cert.org/vuls/id/612636 http://people.irisa.fr/Thomas.Genet/span/ https://tamarin-prover.github.io REFERENCES 59