Quiz (Formal methods for Security) Flashcards
What are the advantages of static policy checking?
- no runtime overhead
- prevention before deployment
What are advantages of dynamic policy enforcement?
- scalability
- no false alarms
What is Functional Requirements?
Defines how a system is supposed to operate in normal environments
What is Security Requirements?
the constraints of functional requirements to protect the assets from threats
Why formalization?
- provides systematic representation for policies
- enables using existing tools to check whether a policy is satisfied or violated
What is BNF?
- A notation to recursively define policies
- A generic structured language model to define your own language
What is parsing?
the process of working out if a given statement is valid according to the given BNF production rules
What is LTL?
Linear-time Temporal Logic. A logic for reasoning about execution paths of systems
The unary connectives have higher precedence than the binary connectives. T/F
True
What is MTL?
Metric Temporal Logic
- LTL + Timing constraints (non-negative real number) on temporal operators
How to model a system?
- Manual effort (physics-based modeling)
- Program analysis
- Trace-based methods (perfume, system identification)
What are some verification methods?
- model checking (exhaustive but not scalable)
- testing (not exhaustive but scalable)
- optimization-guided falsification (trade-off)
What is model checking?
Given a system model (usually FSM) and a policy, outputs the policy is true on the system or presents a counterexample.
What is testing?
Execute the system with a finite set of inputs and check whether the policies are satisfied or violated in their traces.
Why testing?
- model checking of MTL policies on timed and hybrid automata are undecidable
- testing offers a more scalable option for validation
What is falsification?
the process of intelligently selecting test inputs to expose policy violations
Why falsification?
Testing has no feedback mechanism
What is robustness?
numerically quantifies how close the system is to a policy violation
What are some components of the dynamic policy enforcement?
- state (trace/log) collection
- prediction
- run-time policy checking
- response to violations
What is state (trace/log) collection?
Collect the physical states and internal variables from software for prediction and policy checking.
What is run-time policy checking?
Check whether a policy is satisfied or violated during the system is running.
What are some challenges of runtime policy checking?
- at time t, we only have states from {…, t-2, t-1, t}
- we cannot check policies related to future
What are some solutions to the challenges of runtime policy checking?
- use temporal logic with unbounded past and bounded future
- use models to predict the bounded future states
What are the goals to responses to violations?
- prevent policy violation
- recovery
