\commentout{ \begin{code} module HighAssurance where import Classic import Enigma \end{code} } %##################################################################### \chapter{High-assurance programming} \label{cha:high-assur-progr} Writing correct software is the holy grail of programming. Bugs inevitably exist, however, even in thoroughly tested projects. One fundamental issue is the lack of support in typical programming languages to let the programmer \emph{state} what it means to be correct, let alone formally establish any notion of correctness. To address this shortcoming, Cryptol advocates the high-assurance programming approach: programmers explicitly state correctness properties\indProperty along with their code, which are explicitly checked by the Cryptol toolset. Properties are not comments or mere annotations, so there is no concern that they will become obsolete as your code evolves. The goal of this chapter is to introduce you to these tools, and to the notion of high-assurance programming in Cryptol via examples. %===================================================================== % \section{Writing properties} % \label{sec:writingproperties} \sectionWithAnswers{Writing properties}{sec:writingproperties} Consider the equality: $$ x^2 - y^2 = (x-y) * (x+y) $$ Let us write two Cryptol functions that capture both sides of this equation:\indTimes\indExponentiate\indMinus\indPlus \begin{code} sqDiff1 (x, y) = x^^2 - y^^2 sqDiff2 (x, y) = (x-y) * (x+y) \end{code} We would like to express the property that {\tt sqDiff1} and {\tt sqDiff2} are precisely the same functions: Given the same {\tt x} and {\tt y}, they should return exactly the same answer. We can express this property in Cryptol using a {\tt properties} declaration:\indProperty \begin{code} sqDiffsCorrect : ([8], [8]) -> Bit property sqDiffsCorrect (x, y) = sqDiff1 (x, y) == sqDiff2 (x, y) \end{code} The above declaration reads as follows: {\tt sqDiffsCorrect} is a property stating that for all {\tt x} and {\tt y}, the expression {\tt sqDiff1 (x, y) == sqDiff2(x, y)} evaluates to {\tt True}. Furthermore, the type signature restricts the type of the property to apply to only 8-bit values. As usual, the type signature is optional.\indSignature If not given, Cryptol will infer one for you. \begin{Exercise}\label{ex:thm:intro} Put the above property in a file and load it into Cryptol. Then issue the command: \begin{Verbatim} Cryptol> :t sqDiffsCorrect \end{Verbatim} What do you see?\indCmdInfo \end{Exercise} \begin{Answer}\ansref{ex:thm:intro} Cryptol will print the property location, name, and the type. The command {\tt :i} stands for {\tt info}. It provides data about the properties, type-synonyms, etc. available at the top-level of your program.\indCmdInfo \end{Answer} \note{It is important to emphasize that the mathematical equality above and the Cryptol property are \emph{not} stating precisely the same property. Remember that all Cryptol arithmetic is modular,\indModular while the mathematical equation is over arbitrary numbers, including negative, real, or even complex numbers. The takeaway of this discussion is that we are only using this example for illustration purposes: Cryptol properties relate to Cryptol programs, and should not be used for expressing mathematical theorems (unless, of course, you are stating group theory theorems or theorems in an appropriate algebra)! In particular, {\tt sqDiffsCorrect} is a property about the Cryptol functions {\tt sqDiff1} and {\tt sqDiff2}, not about the mathematical equation that inspired it.} \begin{Exercise}\label{ex:thm:0} Write a property {\tt revRev} stating that {\tt reverse} of a {\tt reverse} returns a sequence unchanged.\indReverse \end{Exercise} \begin{Answer}\ansref{ex:thm:0}\indReverse \begin{code} property revRev xs = reverse (reverse xs) == xs \end{code} \end{Answer} \begin{Exercise}\label{ex:thm:1} Write a property {\tt appAssoc} stating that append is an associative operator.\indAppend \end{Exercise} \begin{Answer}\ansref{ex:thm:1}\indAppend \begin{code} property appAssoc (xs, ys, zs) = xs # (ys # zs) == (xs # ys) # zs \end{code} \end{Answer} \begin{Exercise}\label{ex:thm:2} Write a property {\tt revApp} stating that appending two sequences and reversing the result is the same as reversing the sequences and appending them in the reverse order, as illustrated in the following expression:\indReverse\indAppend \begin{Verbatim} reverse ("HELLO" # "WORLD") == reverse "WORLD" # reverse "HELLO" \end{Verbatim} \end{Exercise} \begin{Answer}\ansref{ex:thm:2}\indReverse\indAppend \begin{code} property revApp (xs, ys) = reverse (xs # ys) == reverse ys # reverse xs \end{code} \end{Answer} \begin{Exercise}\label{ex:thm:3} Write a property {\tt lshMul} stating that shifting left by $k$ is the same as multiplying by $2^k$. \end{Exercise} \begin{Answer}\ansref{ex:thm:3} \begin{code} property lshMul (n, k) = n << k == n * 2^^k \end{code} \end{Answer} \note{A \texttt{property} declaration simply introduces a property about your program, which may or may \emph{not} actually hold. It is an assertion about your program, without any claim of correctness. In particular, you can clearly write properties that simply do not hold:} \begin{code} property bogus x = x != x \end{code} It is important to distinguish between \emph{stating} a property and actually \emph{proving} it. So far, our focus is purely on specification. We will focus on actual proofs in Section~\ref{sec:establishcorrectness}. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Property--function correspondence}\indThmFuncCorr \label{sec:prop-funct-corr} In Cryptol, properties can be used just like ordinary definitions: \begin{Verbatim} Cryptol> sqDiffsCorrect (3, 5) True Cryptol> :t sqDiffsCorrect sqDiffsCorrect : ([8],[8]) -> Bit \end{Verbatim} That is, a property over {\tt$(x, y)$} is the same as a function over the tuple {\tt (x, y)}. We call this the property--function correspondence. Property declarations, aside from the slightly different syntax, are \emph{precisely} the same as Cryptol functions whose return type is \texttt{Bit}. There is no separate language for writing or working with properties. We simply use the full Cryptol language write both the programs and the properties that they satisfy. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Capturing test vectors} \label{sec:thmvec} One nice application of Cryptol properties is in capturing test vectors:\indZero \begin{code} property inctest = [ f x == y | (x, y) <- testVector ] == ~zero where f x = x + 1 testVector = [(3, 4), (4, 5), (12, 13), (78, 79)] \end{code} Notice that the property \texttt{inctest} does not have any parameters (no \emph{forall} section), and thus acts as a simple \texttt{Bit} value that will be true precisely when the given test case succeeds. \todo[inline]{Figure out how to re-run Cryptol in this chapter to make sure the tweak to the above example (removal of dummy single formal parameter) works.} %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Polymorphic properties} \label{sec:polythm} Just like functions, Cryptol properties can be polymorphic as well. If you want to write a property for a polymorphic function, for instance, your properties will naturally be polymorphic too. Here is a simple trivial example: \begin{code} property multShift x = x * 2 == x << 1 \end{code} If we ask Cryptol the type of {\tt multShift}, we get: \begin{Verbatim} Cryptol> :t multShift multShift : {a} (fin a, a >= 2) => [a] -> Bit \end{Verbatim} That is, it is a property about all words of size at least two. The question is whether this property does indeed hold? In the particular case of {\tt multShift} that is indeed the case, below are some examples using the property--function correspondence:\indThmFuncCorr \begin{Verbatim} Cryptol> multShift (5 : [8]) True Cryptol> multShift (5 : [10]) True Cryptol> multShift (5 : [16]) True \end{Verbatim} However, this is \emph{not} always the case for all polymorphic Cryptol properties! The following example demonstrates: \begin{code} property flipNeverIdentity x = x != ~x \end{code} The property {\tt flipNeverIdentity} states that complementing\indComplement the bits of a value will always result in a different value: a property we might expect to hold intuitively. Here is the type of {\tt flipNeverIdentity}: \begin{Verbatim} Cryptol> :t flipNeverIdentity flip : {a} (fin a) => a -> Bit \end{Verbatim} So, the only requirement on {\tt flipNeverIdentity} is that it receives some finite type.\indFin Let us try some examples: \begin{Verbatim} Cryptol> flipNeverIdentity True True Cryptol> flipNeverIdentity 3 True Cryptol> flipNeverIdentity [1 2] True \end{Verbatim} However: \begin{Verbatim} Cryptol> flipNeverIdentity (0 : [0]) False \end{Verbatim} That is, when given a {\tt 0}-bit wide value, the complement will in fact do nothing and return its argument unchanged! Therefore, the property {\tt flipNeverIdentity} is not valid, since it holds at certain monomorphic types, but not at all types.\indMonomorphism \begin{Exercise}\label{ex:polythm:1} Demonstrate another monomorphic type where {\tt flipNeverIdentity} does \emph{not} hold. \end{Exercise} \begin{Answer}\ansref{ex:polythm:1} There are many such types, all sharing the property that they do not take any space to represent. Here are a couple examples:\indZero \begin{Verbatim} Cryptol> flipNeverIdentity (zero : ([0], [0])) False Cryptol> flipNeverIdentity (zero : [0][8]) False \end{Verbatim} \end{Answer} \note{The moral of this discussion is that the notion of polymorphic validity\indThmPolyvalid (i.e., that a given polymorphic property will either hold at all of its monomorphic instances or none) does not hold in Cryptol. A polymorphic property can be valid at some, all, or no instances of it.} \begin{Exercise}\label{ex:polythm:2} The previous exercise might lead you to think that it is the 0-bit word type ({\tt [0]}) that is at the root of the polymorphic validity issue. This is not true. Consider the following example:\indWidth\indThmPolyvalid \begin{code} property widthPoly x = (w == 15) || (w == 531) where w = width x \end{code} What is the type of {\tt widthPoly}? At what instances does it hold? Write a property {\tt evenWidth} that holds only at even-width word instances. \end{Exercise} \begin{Answer}\ansref{ex:polythm:2} \begin{Verbatim} Cryptol> :t widthPoly widthPoly : {a, b} (fin a) => [a]b -> Bit \end{Verbatim} It is easy to see that {\tt widthPoly} holds at the instances: \begin{Verbatim} {b} [15]b -> Bit \end{Verbatim} and \begin{Verbatim} {b} [531]b -> Bit \end{Verbatim} but at no other. Based on this, we can write {\tt evenWidth} as follows:\indWidth \begin{code} property evenWidth x = (width x) ! 0 == False \end{code} remembering that the 0'th bit of an even number is always {\tt False}. We have: \begin{Verbatim} Cryptol> evenWidth (0:[1]) False Cryptol> evenWidth (0:[2]) True Cryptol> evenWidth (0:[3]) False Cryptol> evenWidth (0:[4]) True Cryptol> evenWidth (0:[5]) False \end{Verbatim} \end{Answer} %===================================================================== % \section{Establishing correctness} % \label{sec:establishcorrectness} \sectionWithAnswers{Establishing correctness}{sec:establishcorrectness} Our focus so far has been using Cryptol to \emph{state} properties of our programs, without actually trying to prove them correct. This separation of concerns is essential for a pragmatic development approach. Properties act as contracts that programmers state along with their code, which can be separately checked by the toolset~\cite{erkok-matthews-cryptolEqChecking-09}. This approach allows you to state the properties you want, and then work on your code until the properties are indeed satisfied. Furthermore, properties stay with your program forever, so they can be checked at a later time to ensure changes (improvements/additions/optimizations etc.) did not violate the stated properties. %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Formal proofs} \label{sec:formal-proofs} Recall our very first property, {\tt sqDiffsCorrect}, from Section~\ref{sec:writingproperties}. We will now use Cryptol to actually prove it automatically. To prove {\tt sqDiffsCorrect}, use the command {\tt :prove}:\indCmdProve \begin{Verbatim} Cryptol> :prove sqDiffsCorrect Q.E.D. \end{Verbatim} Note that the above might take a while to complete, as a formal proof is being produced behind the scenes. Once Cryptol formally establishes the property holds, it prints ``{\tt Q.E.D.}'' to tell the user the proof is complete.\indQED\indProve \note{Cryptol uses off-the-shelf SAT\glosSAT and SMT\glosSMT solvers to perform these formal proofs~\cite{erkok-matthews-cryptolEqChecking-09}. By default, Cryptol will use Microsoft Research's Z3 SMT solver under the hood, but it can be configured to use other SAT/SMT solvers as well, such as SRI's Yices~\cite{YicesWWW}\indYices, or CVC4 ~\cite{cvc4WWW}\footnote{To do this, first install the package(s) from the URLs provided in the bibliography. Once a prover has been installed you can activate it with, for example, {\tt :set prover=cvc4}.}. Note that the {\tt :prove} command is a push-button tool: once the proof starts there is no user involvement. Of course, the external tool used may not be able to complete all the proofs in a feasible amount of time, naturally. \todo[inline]{Is this going to be a SAW-only capability, or Cryptol as well? Ensure that a ticket exists for forward-porting this functionality.} % While it is out of the scope of this book, let us also mention that % Cryptol can also translate properties to Isabelle/HOL\indIsabelleHOL % for semi-automated theorem proving purposes~\cite{Isabelle-book}, % where more complicated properties can be tackled with the human % guidance if necessary. } %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Counterexamples} \label{sec:counterexamples} Of course, properties can very well be invalid, due to bugs in code or the specifications themselves. In these cases, Cryptol will always print a counterexample value demonstrating why the property does not hold. Here is an example demonstrating what happens when things go wrong: \begin{code} failure : [8] -> Bit property failure x = x == x+1 \end{code} We have: \begin{Verbatim} Cryptol> :prove failure failure 0 = False \end{Verbatim} Cryptol tells us that the property is falsifiable, and then demonstrates a particular value ({\tt 0} in this case) that it fails at. These counterexamples are extremely valuable for debugging purposes.\indCounterExample If you try to prove an invalid property that encodes a test vector (Section~\ref{sec:thmvec}), then you will get a mere indication that you have a contradiction, since there are no universally quantified variables to instantiate to show you a counterexample.\indContradiction If the expression evaluates to {\tt True}, then it will be a trivial proof, as expected: \begin{Verbatim} Cryptol> :prove False False = False Cryptol> :prove True Q.E.D. Cryptol> :prove 2 == 3 (2 == 3) = False Cryptol> :prove reverse [1, 2] == [1, 2] (reverse [1, 2] == [1,2]) = False Cryptol> :prove 1+1 == 0 Q.E.D. \end{Verbatim} The very last example demonstrates modular arithmetic in operation, as usual.\indModular %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Dealing with polymorphism} \label{sec:deal-with-polym} As we mentioned before, Cryptol properties can be polymorphic. As we explored before, we cannot directly prove polymorphic properties as they may hold for certain monomorphic instances while not for others. In this cases, we must tell Cryptol what particular monomorphic instance of the property we would like it to prove. Let us demonstrate this with the \texttt{multShift} property from Section~\ref{sec:polythm}: \begin{Verbatim} Cryptol> :prove multShift Not a monomorphic type: {a} (a >= 2, fin a) => [a] -> Bit \end{Verbatim} Cryptol is telling us that it cannot prove a polymorphic property directly. We can, however, give a type annotation to monomorphise it,\indTypeAnnotation and then prove it at a desired instance: \begin{Verbatim} Cryptol> :prove multShift : [16] -> Bit Q.E.D. \end{Verbatim} In fact, you can use this very same technique to pass any bit-valued function to the {\tt :prove} command:\indCmdProve\indWhere \begin{Verbatim} Cryptol> :prove dbl where dbl x = (x:[8]) * 2 == x+x Q.E.D. \end{Verbatim} Of course, a \lamex (Section~\ref{sec:lamex}) would work just as well too:\indLamExp \begin{Verbatim} Cryptol> :prove \x -> (x:[8]) * 2 == x+x Q.E.D. \end{Verbatim} \begin{Exercise}\label{ex:prove:1} Prove the property {\tt revRev} you wrote in Exercise~\ref{sec:writingproperties}-\ref{ex:thm:0}. Try different monomorphic instantiations. \end{Exercise} \begin{Answer}\ansref{ex:prove:1} If we try to prove {\tt revRev} directly, we will get an error from Cryptol: \begin{Verbatim} Cryptol> :prove revRev Not a valid predicate type: {a, b} (fin a, Cmp b) => [a]b -> Bit \end{Verbatim} Cryptol is telling us that the property has a polymorphic type, and hence cannot be proven. We can easily prove instances of it, by either creating new properties with fixed type signatures\indSignature, or by monomorphising it via type annotations\indTypeAnnotation. Several examples are given below: \begin{Verbatim} Cryptol> :prove revRev : [10][8] -> Bit Q.E.D. Cryptol> :prove revRev : [100][32] -> Bit Q.E.D. Cryptol> :prove revRev : [0][4] -> Bit Q.E.D. \end{Verbatim} \end{Answer} \begin{Exercise}\label{ex:prove:2} Prove the property {\tt appAssoc} you wrote in Exercise~\ref{sec:writingproperties}-\ref{ex:thm:1}, at several different monomorphic instances. \end{Exercise} \begin{Exercise}\label{ex:prove:3} Prove the property {\tt revApp} you wrote in Exercise~\ref{sec:writingproperties}-\ref{ex:thm:2}, at several different monomorphic instances. \end{Exercise} \begin{Exercise}\label{ex:prove:4} Prove the property {\tt lshMul} you wrote in Exercise~\ref{sec:writingproperties}-\ref{ex:thm:3}, at several different monomorphic instances. \end{Exercise} \begin{Exercise}\label{ex:prove:5} Use the {\tt :prove} command to prove and demonstrate counterexamples for the property {\tt widthPoly} defined in Exercise~\ref{sec:writingproperties}-\ref{ex:polythm:2}, using appropriate monomorphic instances. \end{Exercise} \begin{Answer}\ansref{ex:prove:5} We have: \begin{Verbatim} Cryptol> :prove widthPoly : [15] -> Bit Q.E.D. Cryptol> :prove widthPoly : [531] -> Bit Q.E.D. Cryptol> :prove widthPoly : [8] -> Bit widthPoly:[8] -> Bit 0 = False Cryptol> :prove widthPoly : [32] -> Bit widthPoly:[32] -> Bit 0 = False \end{Verbatim} \end{Answer} %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \subsection{Conditional proofs} \label{sec:condproof} It is often the case that we are interested in a property that only holds under certain conditions. For instance, in Exercise~\ref{sec:arithmetic}-\ref{ex:arith:5:1} we have explored the relationship between Cryptol's division, multiplication, and modulus operators, where we asserted the following property:\indMod\indDiv\indTimes $$ x = (x / y) \times y + (x\,\%\,y) $$ Obviously, this relationship holds only when $y \not= 0$. The idea behind a conditional Cryptol property\indThmCond is that we would like to capture these side-conditions formally in our specifications. We simply use an ordinary {\tt if-then-else} expression in Cryptol to write conditional properties (at least until we add boolean logic operators to Cryptol). If the condition is invalid, we simply return {\tt True}, indicating that we are not interested in that particular case. Depending on how natural it is to express the side-condition or its negation, you can use one of the following two patterns: % the following looks ODDLY laid out in the source but comes out OK when latex'ed \begin{Verbatim}[commandchars=\\\{\}] if \emph{side-condition-holds} if \emph{side-condition-fails} then \emph{property-expression} then True else True else \emph{property-expression} \end{Verbatim} \begin{Exercise}\label{ex:cond:1} Express the relationship between division, multiplication, and modulus using a conditional Cryptol property. Prove the property for various monomorphic instances.\indMod\indDiv\indTimes\indThmCond \end{Exercise} \begin{Answer}\ansref{ex:cond:1} \begin{code} property divModMul (x,y) = if y == 0 then True // precondition fails => True else x == (x / y) * y + x % y \end{code} We have: \begin{Verbatim} Cryptol> :prove divModMul : ([4], [4]) -> Bit Q.E.D. Cryptol> :prove divModMul : ([8], [8]) -> Bit Q.E.D. \end{Verbatim} \end{Answer} %% TODO: Pedagogy here without exceptions %% \note{It is tempting to write a function:} %% \begin{code} %% implies (a, b) = if a then b else True %%\end{code} %%to simplify writing conditional properties. %% However, this approach is flawed as it fails to account correctly for %% exceptions. We shall revisit this topic in detail in %% Sections~\ref{sec:pitfall:evorder} and~\ref{sec:pitfall:thmexceptions}. \paragraph*{Recognizing messages} Our work on classic ciphers (Chapter~\ref{chapter:classic}) and the enigma (Chapter~\ref{chapter:enigma}) involved working with messages that contained the letters {\tt 'A'} .. {\tt 'Z'} only. When writing properties about these ciphers it will be handy to have a recognizer for such messages, as we explore in the next exercise. \begin{Exercise}\label{ex:cond:2} Write a function: \begin{code} validMessage : {n} (fin n) => String n -> Bit \end{code} that returns {\tt True} exactly when the input only consists of the letters {\tt 'A'} through {\tt 'Z'}. \lhint{Use the functions {\tt all} defined in Exercise~\ref{sec:zero}-\ref{ex:zero:1},\indAll and {\tt elem} defined in Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}.\indElem} \end{Exercise} \begin{Answer}\ansref{ex:cond:2} Using {\tt all}\indAll and {\tt elem}\indElem, it is easy to express {\tt validMessage}: \begin{code} validMessage = all (\c -> elem (c, ['A' .. 'Z'])) \end{code} Note the use of a \lamex to pass the function to {\tt all}. Of course, we could have defined a separate function for it in a {\tt where}-clause\indWhere, but the function is short enough to directly write it inline. \end{Answer} \todo[inline]{Should we revisit directly some past examples or solutions in the appendix and show what kinds of properties are appropriate to write and which ones can be verified?} \begin{Exercise}\label{ex:cond:3} Recall the pair of functions {\tt caesar} and {\tt dCaesar} from Section~\ref{sec:caesar}.\indCaesarscipher Write a property, named {\tt caesarCorrect}, stating that {\tt caesar} and {\tt dCaesar} are inverses of each other for all {\tt d} (shift amount) and {\tt msg} (message)'s. Is your property valid? What extra condition do you need to assert on {\tt msg} for your property to hold? Prove the property for all messages of length 10. \end{Exercise} \begin{Answer}\ansref{ex:cond:3} A naive attempt would be to write: \begin{code} property caesarCorrectBOGUS (d,msg) = dCaesar(d, caesar(d, msg)) == msg \end{code} However, this property is not correct for all {\tt msg}'s, since Caesar's cipher only works for messages containing the letters {\tt 'A'} \ldots {\tt 'Z'}, not arbitrary 8-bit values as the above property suggests. We can see this easily by providing a bad input: \begin{Verbatim} Cryptol> caesar (3, "1") invalid sequence index: 240 \end{Verbatim} (240 is the difference between the ASCII value of {\tt '1'}, 49, and the letter {\tt 'A'}, 65, interpreted as an 8-bit offset.) We should use the {\tt validMessage} function of the previous exercise to write a conditional property instead: \begin{code} property caesarCorrect (d,msg) = if validMessage msg then dCaesar(d, caesar(d, msg)) == msg else True \end{code} We have: \begin{Verbatim} Cryptol> :prove caesarCorrect : ([8], String(10)) -> Bit Q.E.D. \end{Verbatim} \end{Answer} \begin{Exercise}\label{ex:cond:4} Write and prove a property for the {\tt modelEnigma} machine (Page~\pageref{def:modelEnigma}), relating the {\tt enigma} and {\tt dEnigma} functions from Section~\ref{enigma:encdec}. \end{Exercise} \begin{Answer}\ansref{ex:cond:4} \begin{code} property modelEnigmaCorrect pt = if validMessage pt then dEnigma (modelEnigma, enigma (modelEnigma, pt)) == pt else True \end{code} We have: \begin{Verbatim} Cryptol> :prove modelEnigmaCorrect : String(10) -> Bit Q.E.D. \end{Verbatim} \end{Answer} This may take a long time to prove, depending on the speed of your machine, and the prover you choose. %===================================================================== % \section{Automated random testing} % \label{sec:quickcheck} \sectionWithAnswers{Automated random testing}{sec:quickcheck} Cryptol's {\tt :prove} command\indCmdProve constructs rigorous formal proofs using push-button tools.\footnote{While some of the solvers that Cryptol uses are capable of \emph{emitting} proofs, such functionality is not exposed as a Cryptol feature.} The underlying technique used by Cryptol (SAT-\glosSAT and SMT-based\glosSMT equivalence checking) is complete\indProofCompleteness, i.e., it will always either prove the property or find a counterexample.\indCounterExample In the worst case, however, the proof process might take infeasible amounts of resources, potentially running out of memory or taking longer than the amount of time you are willing to wait. What is needed for daily development tasks is a mechanism to gain some confidence on the correctness of the properties without paying the price of formally proving them. This is the goal of Cryptol's {\tt :check}\indCmdCheck command, inspired by Haskell's quick-check library~\cite{quickcheck}. Instead of trying to formally prove your property, {\tt :check} tests it at random values to give you quick feedback. This approach is very suitable for rapid development. By using automated testing you get frequent and quick updates from Cryptol regarding the status of your properties, as you work through your code. If you introduce a bug, it is likely (although not guaranteed) that the {\tt :check} command will alert you right away. Once you are satisfied with your code, you can use the {\tt :prove} command to conduct the formal proofs, potentially leaving them running overnight. The syntax of the {\tt :check} command is precisely the same as the {\tt :prove} command. By default, it will run your property over 100 randomly generated test cases. \begin{Exercise}\label{ex:quick:0} Use the {\tt :check} command to test the property {\tt caesarCorrect} you have defined in Exercise~\ref{sec:condproof}-\ref{ex:cond:2}, for messages of length 10. Use the command {\tt :set tests=1000}\indQCCount to change the number of test cases to 1,000. Observe the test coverage statistics reported by Cryptol. How is the total number of cases computed? \end{Exercise} \begin{Answer}\ansref{ex:quick:0} Here is the interaction with Cryptol (when you actually run this, you will see the test cases counting up as they are performed):\indQCCount \begin{Verbatim} Cryptol> :check (caesarCorrect : ([8], String 10) -> Bit) Using random testing. passed 100 tests. Coverage: 0.00% (100 of 2^^88 values) Cryptol> :set tests=1000 Cryptol> :check (caesarCorrect : ([8], String 10) -> Bit) Using random testing. passed 1000 tests. Coverage: 0.00% (1000 of 2^^88 values) \end{Verbatim} In each case, Cryptol tells us that it checked a minuscule portion of all possible test cases: A good reminder of what {\tt :check} is really doing. The number of test cases is: $2^{8+8\times10} = 2^{88}$. We have 8-bits for the {\tt d} value, and $10*8$ bits total for the 10 characters in {\tt msg}, giving us a total of 88 bits. Since the input is 88 bits wide, we have $2^{88}$ potential test cases. Note how the number of test cases increase exponentially with the size of the message. \end{Answer} \begin{Exercise}\label{ex:quick:1} If the property is \emph{small} in size, {\tt :check} might as well prove/disprove it. Try the following commands: \begin{Verbatim} :check True :check False :check \x -> x==(x:[8]) \end{Verbatim} \end{Exercise} \begin{Answer}\ansref{ex:quick:1} \begin{Verbatim} Cryptol> :check True Using exhaustive testing. passed 1 tests. QED Cryptol> :check False Using exhaustive testing. FAILED for the following inputs: Cryptol> :check \x -> x == (x:[8]) Using exhaustive testing. passed 256 tests. QED \end{Verbatim} Note that when Cryptol is able to exhaust all possible inputs, it returns QED, since the property is effectively proven. \end{Answer} \begin{Exercise}\label{ex:quick:2} Write a bogus property that will be very easy to disprove using {\tt :prove}, while {\tt :check} will have a hard time obtaining the counterexample. The moral of this exercise is that you should try {\tt :prove} early in your development and not get too comfortable with the results of {\tt :check}!\indCmdProve\indCmdCheck \end{Exercise} \begin{Answer}\ansref{ex:quick:2} \begin{code} property easyBug x = x != (76123:[64]) \end{code} The {\tt :prove} command will find the counterexample almost instantaneously, while {\tt :check} will have a hard time! \end{Answer} \paragraph*{Bulk operations} If you use {\tt :check}\indCmdCheck and {\tt :prove}\indCmdProve commands without any arguments, Cryptol will check and prove all the properties defined in your program. This is a simple means of exercising all your properties automatically. \todo[inline]{Do we want to reintroduce the \texttt{-n} switch, per \ticket{276}?} %% \paragraph*{Automatic invocation} You will notice that Cryptol will %% automatically {\tt :check} the properties in your file when you %% load the file from the command line, giving you a quick status %% report. You can turn this behavior off by passing Cryptol the flag %% {\tt -n}, like this: {\tt cryptol -n myfile.cry}. You can also %% interrupt a running {\tt :prove}\indCmdProve or {\tt %% :check}\indCmdCheck command by pressing {\tt %% Ctrl-C}.\indCmdAutoCheck %===================================================================== % \section{Checking satisfiability} % \label{sec:sat} \sectionWithAnswers{Checking satisfiability}{sec:sat} Closely related to proving properties is the notion of checking satisfiability. In satisfiability checking,\indCmdSat we would like to find arguments to a bit-valued function such that it will evaluate to {\tt True}, i.e., it will be satisfied.\indSat One way to think about satisfiability checking is \emph{intelligently} searching for a solution. Here is a simple example. Let us assume we would like to compute the modular square-root of 9 as an 8-bit value. The obvious solution is {\tt 3}, of course, but we are wondering if there are other solutions to the equation $x^2 \equiv 9 \imod{2^8}$. To get started, let us first define a function that will return {\tt True} if its argument is a square-root of 9: \begin{code} isSqrtOf9 : [8] -> Bit isSqrtOf9 x = x*x == 9 \end{code} Any square-root of 9 will make the function {\tt isSqrtOf9} return {\tt True}, i.e., it will \emph{satisfy} it. Thus, we can use Cryptol's satisfiability checker to find those values of {\tt x} automatically: \begin{Verbatim} Cryptol> :sat isSqrtOf9 isSqrtOf9 3 = True \end{Verbatim} Not surprisingly, Cryptol told us that 3 is one such value. We can search for other solutions by explicitly disallowing 3: \begin{Verbatim} Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3])) \x -> isSqrtOf9 x && ~(elem (x, [3])) 131 = True \end{Verbatim} Note the use of the \lamex to\indLamExp indicate the new constraint. (Of course, we could have defined another function {\tt isSqrtOf9ButNot3} for the same effect, but the \lamex is really handy in this case.) We have used the function {\tt elem} you have defined in Exercise~\ref{sec:recandrec}-\ref{ex:recfun:4:1}\indElem to express the constraint {\tt x} must not be 3. In response, Cryptol told us that {\tt 125} is another solution. Indeed $125 * 125 = 9\imod{2^7}$, as you can verify separately. We can search for more: \begin{Verbatim} Cryptol> :sat \x -> isSqrtOf9 x && ~(elem (x, [3, 125])) \x -> isSqrtOf9 x && ~(elem (x, [3, 131])) 253 = True \end{Verbatim} Rather than manually adding solutions we have already seen, we can search for other solutions by asking the satisfiability checker for more solutions using the {\tt satNum} setting: \begin{Verbatim} Cryptol> :set satNum = 4 Cryptol> :sat isSqrtOf9 isSqrtOf9 3 = True isSqrtOf9 131 = True isSqrtOf9 125 = True isSqrtOf9 253 = True \end{Verbatim} By default, {\tt satNum} is set to {\tt 1}, so we only see one solution. When we change it to {\tt 4}, the satisfiability checker will try to find \emph{up to} 4 solutions. We can also set it to {\tt all}, which will try to find as many solutions as possible. \begin{Verbatim} Cryptol> :set satNum = all Cryptol> :sat isSqrtOf9 isSqrtOf9 3 = True isSqrtOf9 131 = True isSqrtOf9 125 = True isSqrtOf9 253 = True \end{Verbatim} So, we can rest assured that there are exactly four 8-bit square roots of 9; namely 3, 131, 125, and 253. (Note that Cryptol can return the satisfying solutions in any order depending on the backend-solver and other configurations. What is guaranteed is that you will get precisely the same set of solutions at the end.) The whole point of the satisfiability checker is to be able to quickly search for particular values that are solutions to potentially complicated bit-valued functions. In this sense, satisfiability checking can also be considered as an automated way to invert a certain class of functions, going back from results to arguments. Of course, this search is not done blindly, but rather using SAT\glosSAT and SMT\glosSMT solvers to quickly find the satisfying values. Cryptol's {\tt :sat} command\indCmdSat hides the complexity, allowing the user to focus on the specification of the problem. \todo[inline]{Re-add chapter on verification, or two chapters on \texttt{:sat} and \texttt{:prove}.} % (We will see several larger applications of the satisfiability % checker in Chapter~\ref{chap:usingsat}.) \begin{Exercise}\label{ex:sat:0} Fermat's last theorem states that there are no integer solutions to the equation $a^n + b^n = c^n$ when $a, b, c > 0,$ and $n > 2$. We cannot code Fermat's theorem in Cryptol since we do not have arbitrary integers, but we can code the modular version of it where the exponentiation and addition is done modulo a fixed bit-size. Write a function {\tt modFermat} with the following signature: \begin{code} type Quad a = ([a], [a], [a], [a]) modFermat : {s} (fin s, s >= 2) => Quad s -> Bit \end{code} such that {\tt modFermat (a, b, c, n)} will return {\tt True} if the modular version of Fermat's equation is satisfied by the values of {\tt a}, {\tt b}, {\tt c}, and {\tt n}. Can you explain why you need the constraints {\tt fin s} and {\tt s >= 2}? \end{Exercise} \begin{Answer}\ansref{ex:sat:0} \begin{code} modFermat (a, b, c, n) = (a > 0) && (b > 0) && (c > 0) && (n > 2) && (a^^n + b^^n == c^^n) \end{code} The {\tt fin s} predicate comes from the fact that we are doing arithmetic and comparisons. The predicate {\tt s >= 2} comes from the fact that we are comparing {\tt n} to {\tt 2}, which needs at least $2$ bits to represent. \end{Answer} \begin{Exercise}\label{ex:sat:1} Use the {\tt :sat} command to see if there are any satisfying values for the modular version of Fermat's last theorem for various bit sizes. Surprised? What can you conclude from your observations? \end{Exercise} \begin{Answer}\ansref{ex:sat:1} We can try different instantiations as follows: \begin{Verbatim} Cryptol> :sat modFermat : Quad(2) -> Bit modFermat : Quad(2) -> Bit (1, 2, 1, 3) = True Cryptol> :sat modFermat : Quad(3) -> Bit modFermat : Quad(3) -> Bit (4, 4, 4, 4) = True Cryptol> :sat modFermat : Quad(4) -> Bit modFermat : Quad(4) -> Bit (4, 4, 4, 8) = True \end{Verbatim} The modular form of Fermat's last theorem does not hold for any of the instances up to and including 12-bits wide, when I stopped experimenting myself. It is unlikely that it will hold for any particular bit-size, although the above demonstration is not a proof. (We would need to consult a mathematician for the general result!) Also note that Cryptol takes longer and longer to find a satisfying instance as you increase the bit-size. \end{Answer} %===================================================================== %% \section{Safety checking} %% \label{sec:safetychecking} %% Safety checking is all about run-time exceptions: Division-by-zero %% or index-out-of-bounds being the most infamous ones. Unlike many %% other languages, Cryptol does not suffer from a certain class of %% safety violations, such as trying to put in the number 1000 in a %% buffer that is only 8-bits wide, or trying to multiply a string %% with an integer; but certain run-time exceptions are still %% possible. The goal of \emph{safety checking} is to ensure that these %% exceptions cannot happen at run-time.\indSafe\indCmdSafe %% Here is a simple example to demonstrate: %% \begin{Verbatim} %% Cryptol> :safe \(x, y) -> x/y:[8] %% *** 1 safety condition to be checked. %% *** Checking for violations of: ``"command line", line 1, col 13: divide by zero'' %% *** Violation detected: %% (\(x, y) -> x/y:[8]) (0, 0) %% = "command line", line 1, col 14: divide by zero %% *** 1 problem found. %%\end{Verbatim} %%Cryptol is telling us that the function {\tt $\backslash$(x, y) -> %% x/y} is \emph{not} safe. When given the argument {\tt (0, 0)} it %% will cause a division by zero exception. If we properly guard for %% the condition, then the safety check will indeed pass: %%\begin{Verbatim} %% Cryptol> :safe \(x, y) -> if y == 0 then 0 else x/y:[8] %% *** 1 safety condition to be checked. %% *** Checking for violations of: ``"command line", line 1, col 35: divide by zero'' %% *** Verified safe. %% *** All safety checks pass, safe to execute %%\end{Verbatim} %%By using {\tt :safe}\indCmdSafe on our top-level functions we can %% ensure that our program is guaranteed not to have any run-time %% exceptions. Cryptol's safety-checker will detect the following %% run-time exceptions: %%\begin{itemize} %% \item Division ({\tt /}) and modulus ({\tt \%}) by 0, both modular %% and polynomial versions (See %% Section~\ref{sec:polynomials})\indDiv\indMod\indDivPoly\indModPoly %% \item Index-out-of-bounds errors for {\tt @}, {\tt @@}, {\tt !} and %% {\tt !!},\indIndex\indIndexs\indRIndex\indRIndexs %% \item Calling {\tt lg2} on {\tt 0},\indLg %% \item Data dependence on {\tt error} and the {\tt undefined} %% values,\indError\indUndefined %% \item Failure cases for Cryptol's {\tt ASSERT} %% expression.\indAssert %%\end{itemize} %%\begin{Exercise}\label{ex:safe:0} %%Consider the function: %%\begin{code} %% lkup : ([10][8], [4]) -> [8] %% lkup (xs, i) = xs @ i %%\end{code} %%Is it safe? For what values of {\tt i} does it throw an exception? %%\end{Exercise} %%\begin{Answer}\ansref{ex:safe:0} %% {\tt lkup} will throw an exception whenever {\tt i} is at least %% {\tt 10}. We can use Cryptol to detect this safety violation: %%\begin{Verbatim} %% Cryptol> :safe lkup %% *** 1 safety condition to be checked. %% *** Checking for violations of: ``..: index of symbolic-value is out of bounds %% (valid range is 0 thru 9).'' %% *** Violation detected: %% lkup ([255 255 255 255 255 255 255 255 255 255], 13) %% = .. index of 13 is out of bounds %% (valid range is 0 thru 9). %% *** 1 problem found. %%\end{Verbatim} %%In this case Cryptol identified that there will be an exception when %% {\tt i} is 13. %%\end{Answer} %%\begin{Exercise}\label{ex:safe:1} %%Here is an attempt to make {\tt lkup} safe: %%\begin{code} %% lkup1 : ([10][8], [4]) -> [8] %% lkup1 (xs, i) = if i > 10 then 0 else xs @ i %%\end{code} %%Is the fix successful? Use the {\tt :safe} command to check your %% answer. %%\end{Exercise} %%\begin{Answer}\ansref{ex:safe:1} %%No. {\tt lkup1} suffers from the infamous off-by-1 error! %%\begin{Verbatim} %% Cryptol> :safe lkup1 %% *** 1 safety condition to be checked. %% *** Checking for violations of: ``..: index of symbolic-value is out of bounds %% (valid range is 0 thru 9).'' %% *** Violation detected: %% lkup1 ([255 255 255 255 255 255 255 255 255 255], 10) %% = ..: index of 10 is out of bounds %% (valid range is 0 thru 9). %% *** 1 problem found. %%\end{Verbatim} %%This time Cryptol will pin-point to the only potential error value, %% where {\tt i} is 10. %%\end{Answer} %% %%\begin{Exercise}\label{ex:safe:2} %% Write a version of {\tt lkup} that fixes the safety issue. Use the %% {\tt :safe} command to verify that your fix is good. %%\end{Exercise} %%\begin{Answer}\ansref{ex:safe:2} %%\begin{code} %% lkup2 : ([10][8], [4]) -> [8] %% lkup2 (xs, i) = if i > 9 then 0 else xs @ i %%\end{code} %%We have: %%\begin{Verbatim} %% Cryptol> :safe lkup2 %% *** 1 safety condition to be checked. %% *** Checking for violations of: ``..: index of symbolic-value is out of bounds %% (valid range is 0 thru 9).'' %% *** Verified safe. %% *** All safety checks pass, safe to execute. %%\end{Verbatim} %%\end{Answer} %% %%\paragraph*{Over-conservative safety checking} %% Cryptol's safety checker is very conservative: If it says that a %% function is \emph{safe to execute}, you are guaranteed that the %% execution can not raise any run-time exception. However, the %% converse is not always true: In certain cases, Cryptol can signal a %% potential safety violation which will actually not cause an error %% when \emph{run in the normal interpreter}. %% %% Here is an example to illustrate the idea. (The example is somewhat %% contrived, but similar patterns of coding does arise in Cryptol %% programming.) We will use Cryptol's {\tt undefined} %% value\indUndefined, which would throw an exception if executed: %%\begin{Verbatim} %% Cryptol> (1:[8]) + undefined %% Entered Cryptol 'undefined' value %%\end{Verbatim} %% %%Cryptol's {\tt undefined}\indUndefined is useful when representing %% values that should \emph{not} be needed during execution, as %% illustrated below: %%\begin{code} %% choose : [8] -> [8] %% choose c = ([undefined] # [1 ..]) @ index %% where index = if c == 0 then 1 else c %%\end{code} %%Notice that {\tt undefined} will not be referenced: The {\tt index} %% can never be {\tt 0}. (Why?) If we ask {\tt :safe}, though, it will %% tell us the following: %%\begin{Verbatim} %% Cryptol> :safe choose %% *** 1 safety condition to be checked. %% *** Checking for violations of: ``Entered Cryptol 'undefined' value'' %% *** Violation detected: %% choose 0 %% = 1 %% *** ALERT: This safety issue is only relevant for certain target platforms %% *** and hence does not cause an exception in the above run. %% *** C and hardware translations might be subject to stricter semantics. %% *** 1 problem found. %%\end{Verbatim} %%The {\tt :safe} command\indCmdSafe told us that there is a safety %% violation when {\tt c} is {\tt 0}, then it also showed us that if %% we run {\tt choose} with {\tt 0} we get the value {\tt 1}, not an %% exception. At first, this sounds quite counterintuitive. However, %% the {\tt ALERT} given by Cryptol sheds some light into the %% potential problem. When Cryptol is used in the normal interpreter %% mode, this program will indeed not produce any exceptions. However, %% Cryptol programs can also be compiled to other targets, such as C %% or Java, or other hardware platforms. What Cryptol is telling us is %% that these translations are \emph{not} guaranteed to be exception %% free, and hence it is worth making sure the generated code will %% behave properly. %% %% While it is important to understand what Cryptol is telling us, the %% user can safely ignore these alerts most of the time, especially %% when one is focusing only at the Cryptol level. (We will revisit %% this topic in Section~\ref{sec:pitfall:thmexceptions}.) %% %%\begin{Exercise}\label{ex:safe:3} %% Rewrite {\tt choose} so that {\tt :safe} will not issue any %% alerts. %%\end{Exercise} %%\begin{Answer}\ansref{ex:safe:3} %% One way would be to replace {\tt undefined}\indUndefined with {\tt %% zero}.\indZero Since the result will never be needed, we can %% safely replace it with {\tt 0} without changing the semantics. %%\end{Answer} %%% Local Variables: %%% mode: latex %%% TeX-master: "../main/Cryptol" %%% End: