CIS 301: Lecture Notes on Logic for SecurityTorben AmtoftDepartment of Computing and Information SciencesKansas State UniversityDecember 7, 2003These notes are inspired by [1].1 Secure Information FlowAssume we are dealing with two kinds of variables: those of high security (clas-sified); and those of low security (non-classified). Our goal is that users withlow clearance should not be able to gain information about the values of theclassified variables. In the following, this notion will be made precise.For the sake of simplicity, let us assume that there are only two variablesin play: l (for low) and h (for high). We want to protect ourselves against anattacker (spy) who• knows the initial value of l;• knows the program that is running;• can observe the final value of l;• can not observe intermediate states of program execution.A program is said to be secure if such an attacker cannot detect anything aboutthe initial value of h.1.1 ExamplesThe program below is not secure.l := h + 7 (1)For by subtracting 7 from the final value of l, the attacker gets the initial valueof h. On the other hand, the program below is clearly secure.l := l + 47 (2)1One rotten apple does not always spoil the whole barrel; having the insecureprogram in (1) as a preamble may still yield a secure program as inl := h + 7; l := 27 (3)since we assumed that the attacker cannot observe intermediate values of l.Also the following program is secure:h := l (4)For even though the attacker learns the final value of h (as it equals the initialvalue of l which is known), he is still clueless about the initial value of h.The following program is just a fancy way of writing l := h + 7 (since we donot care about the final value of h)l := 7; while h > 0 do h := h − 1; l := l + 1 od (5)and is therefore insecure. Also, the following program is insecureif h = 6789 then l := 0 else l := 1 fi (6)since if the final value of l is zero, we know that h was initially 6789.1.2 SpecificationBy putting quantifiers in front of Hoare triples, we can formally express security:Definition: The program P is secure iff∀l0∃l1∀h0∃h1{l = l0∧ h = h0}P{l = l1∧ h = h1}To put it another way, the final value (l1) of l must depend only on the initialvalue (l0) of l and not on the initial value (h0) of h.By negating this definition (and applying De Morgan’s laws repeatedly), wearrive at:Observation: The program P is insecure iff∃l0∀l1∃h0¬∃h1{l = l0∧ h = h0}P{l = l1∧ h = h1}To put it another way, a program is insecure if for all possible final values of l,there exists an initial value of h that produces a different final value of l.21.3 Examples RevisitedWe first address the programs that are secure, and show that they do indeedmeet the requirement stated in our Definition. In each case, we are given somel0and must find l1such that∀h0∃h1{l = l0∧ h = h0}P{l = l1∧ h = h1}For the program in (2), we choose l1as l0+ 47; this does the job since∀h0∃h1{l = l0∧ h = h0}l := l + 47{l = l0+ 47 ∧ h = h1}For the program in (3), we can choose l1as 27; for the program in (4), we simplychoose l1as l0.We next address the programs that are not secure, and show (cf. our Ob-servation) that no matter how l1has been chosen, we can find h0such that itdoes not hold that{l = l0∧ h = h0}P{l = l1}For the programs in (1) and (5), we can just pick an h0different from l1− 7,say h0= l1. For clearly it does not hold that{l = l0∧ h = l1}l := h + 7{l = l1}For the program in (6), we proceed by cases on l1: if l1is zero, then we canchoose (among many possibilities) h0to be 2345 since it does not hold that{l = l0∧ h = 2345}if h = 6789 then l := 0 else l := 1 fi{l = 0}Alternatively, if l1is one, then we choose h0to be 6789 since it does not holdthat{l = l0∧ h = 6789}if h = 6789 then l := 0 else l := 1 fi{l = 1}(If l1is neither zero nor one, we can choose any value for h0.)31.4 DeclassificationA severe limitation of our theory is exposed by the last example (6) which isconsidered insecure even though very little information may actually be leakedto the attacker. Think of h as denoting a PIN code, with the attacker testingwhether it happens to be 6789; if the PIN codes were selected randomly, thechance of the test revealing the PIN code is very small (1 to 10,000). It iscurrently an important challenge for research in (language based) security toformalize these considerations!1.5 Data IntegrityWe might consider an alternative interpretation of the variables l and h: ldenotes a licensed entity, whereas h denotes a hacked (untrustworthy) entity.The integrity requirement is now:Licensed data should not depend on hacked data.It is interesting to notice that the framework described on the preceding pagescovers also that situation! In particular, a program satisfies the above integrityrequirement if and only if it is considered secure (according to our Definition).For example, (3) is safe as the licensed variable l will eventually contain 27which does not depend on hacked data, whereas (6) is unsafe as the value of thehacked variable h influences the value of the licensed variable.References[1]´Ad´am Darvas, Reiner H¨ahnle, and David Sands. A theorem proving ap-proach to analysis of secure information flow. In Workshop on Issues in theTheory of Security (WITS’03). Affiliated to ETAPS 2003, Warsaw,