Quiz (Formal methods for Security)

Question 1

What are the advantages of static policy checking?

Answer 1

• no runtime overhead
• prevention before deployment

Question 2

What are advantages of dynamic policy enforcement?

Answer 2

• scalability
• no false alarms

Question 3

What is Functional Requirements?

Answer 3

Defines how a system is supposed to operate in normal environments

Question 4

What is Security Requirements?

Answer 4

the constraints of functional requirements to protect the assets from threats

Question 5

Why formalization?

Answer 5

• provides systematic representation for policies
• enables using existing tools to check whether a policy is satisfied or violated

Question 6

What is BNF?

Answer 6

• A notation to recursively define policies
• A generic structured language model to define your own language

Question 7

What is parsing?

Answer 7

the process of working out if a given statement is valid according to the given BNF production rules

Question 8

What is LTL?

Answer 8

Linear-time Temporal Logic. A logic for reasoning about execution paths of systems

Question 9

The unary connectives have higher precedence than the binary connectives. T/F

Answer 9

True

Question 10

What is MTL?

Answer 10

Metric Temporal Logic
- LTL + Timing constraints (non-negative real number) on temporal operators

Question 11

How to model a system?

Answer 11

• Manual effort (physics-based modeling)
• Program analysis
• Trace-based methods (perfume, system identification)

Question 12

What are some verification methods?

Answer 12

• model checking (exhaustive but not scalable)
• testing (not exhaustive but scalable)
• optimization-guided falsification (trade-off)

Question 13

What is model checking?

Answer 13

Given a system model (usually FSM) and a policy, outputs the policy is true on the system or presents a counterexample.

Question 14

What is testing?

Answer 14

Execute the system with a finite set of inputs and check whether the policies are satisfied or violated in their traces.

Question 15

Why testing?

Answer 15

• model checking of MTL policies on timed and hybrid automata are undecidable
• testing offers a more scalable option for validation

Question 16

What is falsification?

Answer 16

the process of intelligently selecting test inputs to expose policy violations

Question 17

Why falsification?

Answer 17

Testing has no feedback mechanism

Question 18

What is robustness?

Answer 18

numerically quantifies how close the system is to a policy violation

Question 19

What are some components of the dynamic policy enforcement?

Answer 19

• state (trace/log) collection
• prediction
• run-time policy checking
• response to violations

Question 20

What is state (trace/log) collection?

Answer 20

Collect the physical states and internal variables from software for prediction and policy checking.

Question 21

What is run-time policy checking?

Answer 21

Check whether a policy is satisfied or violated during the system is running.

Question 22

What are some challenges of runtime policy checking?

Answer 22

• at time t, we only have states from {…, t-2, t-1, t}
• we cannot check policies related to future

Question 23

What are some solutions to the challenges of runtime policy checking?

Answer 23

• use temporal logic with unbounded past and bounded future
• use models to predict the bounded future states

Question 24

What are the goals to responses to violations?

Answer 24

• prevent policy violation
• recovery