formal methods Flashcards
what are formal methods
the foundations, methods and tools for developing and reasoning about systems
what do formal methods allow us to do
formally check whether a system satisfies defined propertied
identifies vulnerabilities via trying to prove those properties
what are two pros of formal methods
puts system development on a firm mathematical grounding ( viewing protocols as a mathematical object)
addresses inadequacies in penetrate and patch
what are two cons of formal methods
the verify models not the system itself therefore if the model is inaccurate then so will the results
may not specify all system requirements or may specify incorrectly
what is a negative of tools
may require users to interact with them or produce false negatives
why was using penetrate and patch not good
attackers are good at finding and exploiting vulnerabilities
the more interest in protocols means the more vulnerabilities were found and exploited
what are some examples of tls/ssl attacks
BEAST
heartbleed
DROWN
BEAST
exploits how the iv is generated for block ciphers (cbc mode)
heartbleed
exploited to return information it shouldnt e.g. decryption key
DROWN
only worked with ssl v2 so we stopped using it however attackers could force the system to switch to it in order to decrypt the ciphertext
foundations
recipe for formal methods
what are the three things that we need to do in the foundation of formal methods
precisely specify the; system, adversarial environment and security properties
choose the specification language
verify security properties
why do we need to choose the specification language
it defines the system
why must the model for the adversial environment relate to the real world
the system is being used in the real world so it needs to be accurate and trustworthy
how did the contactless emv payments scam work
the phone is tricked into thinking that its making a payment < £100 therefore it doesnt require the phone to be unlocked and the money is taken from your account
when precisely defining the system in the foundation of the formal model what three things do we look at
system design
code level
configuration level
why is the system design important in the foundation
if the design isnt secure then no implementation conforming to it will be
the system (foundation)
protocols that show security
code level (system - foundation)
used to verify the absence of bugs and sometimes deeper properties
configuration level (system - foundation) + example
the implementation of the protocol
e.g. access control policies
what is the adversarial environment
the model of the attacker/ where the system operates
what are some things that we consider about the attacker when defining the adversarial environment
remote/inside
active/passive
corrupt/control protocol participation
system properties
things that the system should satisfy
what are some examples of system properties
system correctness
safety properties
indistinguishable properties
safety properties
ensuring nothing bad happens
e.g. the attacker signing a message without having a signing key
indistinguishable properties
the attacker shouldnt be able to distinguish between two protocols/ encrypted messages
what are two benefits of having indistinguishable properties
allows for confidentiality and anonymity
what are the three types of methods
symbolic
stochastic
computational
symbolic methods
possibilistic security definitions
assumes the dolev-yao attack model
how are protocols defined in symbolic methods
as a transition system based on actions and agents
state model
what are the goals of symbolic methods
confidentiality and authentication
possibilistic
checks whether something bad could happen in theory
dolev-yao attack model
assumes the attacker controls the network and can create their own messages however, cryptography is working perfectly
stochastic methods
assumes the adversary will probably do something wrong
what is a negative of computational methods
more detail means more complexity making it difficult to trust proofs as the model of the system and the attacker may be inaccurate
probalistic
it can make random choices e.g. guessing keys
computational methods
assumes the attackers resources are bounded; they have polynomial time
probalistic
uses detailed and accurate models
several techniques for constructing security proofs
