Class 5: CNF, Quantifiers, and Proofs
Schedule
Problem Set 2 is due Friday at 6:29pm.
Links
If you believe real computing systems have the property that the values you read from memory will match what you wrote there, see:
Sudhakar Govindavajhala and Andrew W. Appel. Using Memory Errors to Attack a Virtual Machine, IEEE Symposium on Security and Privacy 2003.
Bianca Schroeder, Eduardo Pinheiro, Wolf-Dietrich Weber. DRAM Errors in the Wild: A Large-Scale Field Study. SIGMETRICS 2009.
Kaveh Razavi, Ben Gras, Erik Bosman, Bart Preneel, Cristiano Giuffrida and Herbert Bos. Flip Feng Shui: Hammering a Needle in the Software Stack. USENIX Security 2016.
Yuan Xiao, Xiaokuan Zhang, Yinqian Zhang, and Radu Teodorescu. One Bit Flips, One Cloud Flops: Cross-VM Row Hammer Attacks and Privilege Escalation, USENIX Security 2016.
Notes and Questions
Definition: satisfiable. A logical formula is satisfiable if there is some way to make it true. That is, there is at least one assignment of truth value to its variables that makes the forumla true.
Definition: conjunctive normal form (CNF). A logical formula that is written as a conjunction of clauses, where each clause is a disjunction of literals, and each literal is either a variable or a negation of a variable, is in conjunctive normal form. If each clause has excatly three literals, it is called three conjunctive normal form (3CNF).
$$ (a_1 \vee a_2 \vee \neg a_3) \wedge (a_1 \vee \neg a_2 \vee a_3) \wedge (\neg a_1 \vee a_2 \vee \neg a_3) \wedge (\neg a_1 \vee a_2 \vee a_3) $$
##
Show that every logical formula can be written in 3-conjunctive normal form.
What is the maximum number of (different) clauses in a 3CNF formula involving 5 variables?
##
What is the maximum number of (different) clauses in a satisfiable 3CNF formula involving 5 variables?
##
What is the maximum number of (different) clauses in a valid 3CNF formula involving 5 variables?
##
Logical Quantifiers
$\forall x \in S. P(x)$ means $P$ holds for every element of $S$.
$\exists x \in S. P(x)$ means $P$ holds for at least one element of $S$.
Define valid and satisfiable using logical quantifiers:
#
$\forall x \in S. P(x)$ is equivalent to $\neg(\exists x \in S. \qquad \qquad)$
###
Notation: $\textrm{pow}(S)$ denotes the powerset of $S$. The powerset of a set is the set of all possible subsets of that S. So, $\textrm{pow}(\mathbb{N})$ denotes all subsets of the natural numbers.
Notation: $A - B$ denotes the difference between two sets. It is the elements of $A$, with every element of $B$ removed.
Notation: $\varnothing$ is the empty set. It is the set with no elements: ${ }$.
\begin{center} \Large
$$ \fillin S \in \textrm{pow}(\mathbb{N}) - { \varnothing } \ldotp \fillin m \in S\ldotp \fillin x \in S - {m}\ldotp m < x $$
\begin{comment} $$ \forall S \in \textrm{pow}(\mathbb{N}) - { \varnothing } \ldotp \exists m \in S\ldotp \forall x \in S - {m}\ldotp m < x $$ \end{comment} \end{center}
Write a logical expression that captures the meaning of: Proofs can certify that a computing system will always behave correctly, something that no amount of testing can do.
What does it mean to test a computing system? What does it mean for a computing system to always behave correctly?
#