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
