semantics-1: impl

semantics-1/semantics.typ

@@ -17,8 +17,17 @@
 #let ife(e1, e2, e3) = [#kw[if] #e1 #kw[then] #e2 #kw[else] #e3]
 #let suc(e) = [#kw[succ] #e]
 #let prd(e) = [#kw[pred] #e]
+#let sec(e) = [#kw[secret] #e]
 
-// Big-step evaluation relation: e ⇓ v
+// Security labels
+#let lH = $upright(H)$
+#let lL = $upright(L)$
+#let ljoin = $union.sq$
+
+// Labeled value: (v, ℓ)
+#let lval(v, l) = $(#v, #l)$
+
+// Big-step evaluation relation: e ⇓ (v, ℓ)
 #let bstep(e, v) = $#e arrow.b.double #v$
 
 // Rule name label in small-caps
@@ -75,6 +84,9 @@
     #set text(size: 10pt)
     *Abstract.* In this paper, we will provide a review of the big-step operational semantics
     for the BoolInt\* language we discussed in class.
+    We extend the language with a #kw[secret] construct and security labels
+    ($#lH$ for private, $#lL$ for public) to track information flow
+    and prevent secret leakage.
   ]
 ]
 
@@ -94,7 +106,7 @@ expressions always will.)
 // ----- Figure 1: language definition ------------------------
 
 #figure(
-  box(width: 80%, inset: (left: 2em))[
+  box(width: 85%, inset: (left: 2em))[
     #set align(left)
     #mydefhead[$e ::=$ #h(6em)][Expressions]
     #mydefcase(tr, [true value])
@@ -103,6 +115,7 @@ expressions always will.)
     #mydefcase(ife[$e$][$e$][$e$], [conditional expressions])
     #mydefcase(suc[$e$], [successor])
     #mydefcase(prd[$e$], [predecessor])
+    #mydefcase(sec[$e$], [secret])
 
     #v(0.5em)
 
@@ -110,71 +123,120 @@ expressions always will.)
     #mydefcase(tr, [true value])
     #mydefcase(fl, [false value])
     #mydefcase($i$, [integers])
+
+    #v(0.5em)
+
+    #mydefhead[$ell ::=$ #h(6em)][Security Labels]
+    #mydefcase($#lL$, [low / public])
+    #mydefcase($#lH$, [high / private])
   ],
-  caption: [The BoolInt\* language],
+  caption: [The BoolInt\* language with security labels],
 ) <fig:lang>
 
-@fig:lang shows the list of expressions and values for the BoolInt\* language.
+@fig:lang shows the list of expressions, values, and security labels for the BoolInt\* language.
 Expressions can be the value $#tr$, the value $#fl$,
-or the conditional expression $#ife[$e$][$e$][$e$]$.
+integers $i$,
+the conditional expression $#ife[$e$][$e$][$e$]$,
+arithmetic operations $#suc[$e$]$ and $#prd[$e$]$,
+and the security construct $#sec[$e$]$.
 Note that conditional expressions have a recursive structure,
 with 3 sub-expressions.
 
-After evaluating a program, we should be able to produce a value in this language.
+After evaluating a program, we produce a _labeled value_ $#lval[$v$][$ell$]$,
+where $v$ is the value and $ell$ is a security label
+indicating whether the result is public ($#lL$) or private ($#lH$).
 (In other languages, we might hit a bad situation and need to crash instead;
 that won't happen in this language.)
 The valid values for BoolInt\* are $#tr$, $#fl$, and $i$.
 
+We define a _join_ operation $#ljoin$ on security labels as follows:
+$ #lL #ljoin #lL = #lL #h(3em) #lL #ljoin #lH = #lH #ljoin #lL = #lH #ljoin #lH = #lH $
+Intuitively, any interaction with a private value taints the result as private.
+
 With our expressions and values defined,
 we can now specify the semantics for our language.
 To do so, we will use the following big-step evaluation relation:
 
-$ #bstep[$e$][$v$] $
+$ #bstep[$e$][$#lval[$v$][$ell$]$] $
 
-The above line should be read as "the expression $e$ evaluates to the value $v$".
+The above line should be read as
+"the expression $e$ evaluates to the value $v$ with security label $ell$".
 
 // ----- Figure 2: big-step semantics -------------------------
 
 #figure(
-  box(width: 80%, inset: (left: 1em))[
+  box(width: 85%, inset: (left: 1em))[
     #set align(left)
-    #text(weight: "bold")[Evaluation Rules:#h(1em)]#box(stroke: 0.5pt, inset: 4pt, $#bstep[$e$][$v$]$)
+    #text(weight: "bold")[Evaluation Rules:#h(1em)]#box(stroke: 0.5pt, inset: 4pt, $#bstep[$e$][$#lval[$v$][$ell$]$]$)
 
     #v(0.6em)
 
-    #bsrule("B-Value", $emptyset$, $#bstep[$v$][$v$]$)
+    #bsrule("B-Value", $emptyset$, $#bstep[$v$][$#lval[$v$][$#lL$]$]$)
 
-    #bsrule("B-IfTrue", $#bstep[$e_1$][$#tr$] #h(2em) #bstep[$e_2$][$v$]$, $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$)
+    #bsrule("B-Secret", $#bstep[$e$][$#lval[$v$][$ell$]$]$, $#bstep[#sec[$e$]][$#lval[$v$][$#lH$]$]$)
 
-    #bsrule("B-IfFalse", $#bstep[$e_1$][$#fl$] #h(2em) #bstep[$e_3$][$v$]$, $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$v$]$)
+    #bsrule(
+      "B-IfTrue",
+      $#bstep[$e_1$][$#lval[$#tr$][$ell_1$]$] #h(2em) #bstep[$e_2$][$#lval[$v$][$ell_2$]$]$,
+      $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$#lval[$v$][$ell_1 #ljoin ell_2$]$]$,
+    )
 
-    #bsrule("B-Succ", $#bstep[$e$][$i$]$, $#bstep[#suc[$e$]][$i + 1$]$)
+    #bsrule(
+      "B-IfFalse",
+      $#bstep[$e_1$][$#lval[$#fl$][$ell_1$]$] #h(2em) #bstep[$e_3$][$#lval[$v$][$ell_3$]$]$,
+      $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$#lval[$v$][$ell_1 #ljoin ell_3$]$]$,
+    )
 
-    #bsrule("B-Pred", $#bstep[$e$][$i$]$, $#bstep[#prd[$e$]][$i - 1$]$)
+    #bsrule("B-Succ", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#suc[$e$]][$#lval[$i + 1$][$ell$]$]$)
+
+    #bsrule("B-Pred", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#prd[$e$]][$#lval[$i - 1$][$ell$]$]$)
   ],
-  caption: [Big-step semantics for BoolInt\*],
+  caption: [Big-step semantics for BoolInt\* with information flow],
 ) <fig:bigstep>
 
-@fig:bigstep shows the big-step evaluation rules for the BoolInt\* language.
+@fig:bigstep shows the big-step evaluation rules for the BoolInt\* language
-Of course, there are additional possible rules.
+with information flow tracking.
 
 The #rel("B-Value") rule applies when the expression (to the left of "$arrow.b.double$")
 is also a value, as defined in @fig:lang.
 There are no premises for this rule (above the line),
 meaning that it is an _axiom_.
-This rule states that a value evaluates to itself,
+This rule states that a bare value evaluates to itself with a public label $#lL$,
-so that #tr evaluates to #tr and #fl evaluates to #fl.
+so that #tr evaluates to $#lval[$#tr$][$#lL$]$ and $3$ evaluates to $#lval[$3$][$#lL$]$.
+
+The #rel("B-Secret") rule handles the #kw[secret] construct.
+It evaluates the sub-expression $e$ and forces the security label to $#lH$,
+regardless of the original label.
+For example, $#sec[$3$]$ evaluates to $#lval[$3$][$#lH$]$.
 
 Two different rules are needed for handling conditional expressions.
 Which rule applies depends on the premises.
+Critically, both rules _join_ the condition's label $ell_1$ with the branch result's label.
 
 For the #rel("B-IfTrue") rule,
-the premise states that $e_1$ evaluates to #tr
+the premise states that $e_1$ evaluates to $#lval[$#tr$][$ell_1$]$
-and $e_2$ evaluates to some value $v$.
+and $e_2$ evaluates to $#lval[$v$][$ell_2$]$.
-If the premise holds, then the result of evaluating the expression is the value $v$.
+The result carries $ell_1 #ljoin ell_2$ as its label.
 The structure of #rel("B-IfFalse") is similar.
 
+This join is essential for preventing _implicit flows_.
+Consider the expression $#ife[#sec[$#tr$]][$1$][$0$]$.
+Without the join, this would produce $#lval[$1$][$#lL$]$ — leaking which branch was taken
+and thus revealing the secret condition.
+With the join, the condition evaluates to $#lval[$#tr$][$#lH$]$,
+so the result becomes $#lval[$1$][$#lH #ljoin #lL$] = #lval[$1$][$#lH$]$,
+correctly tainting the output as private.
+
 We also have rules for handling the integer operations.
-The #rel("B-Succ") rule states that if the operand $e$ evaluates to an integer $i$,
+The #rel("B-Succ") rule states that if the operand $e$ evaluates to $#lval[$i$][$ell$]$,
-then the expression $#suc[$e$]$ evaluates to $i + 1$.
+then the expression $#suc[$e$]$ evaluates to $#lval[$i + 1$][$ell$]$.
-Similarly, #rel("B-Pred") evaluates $#prd[$e$]$ to $i - 1$ if $e$ evaluates to $i$.
+This propagates the security label faithfully.
+For example, $#suc[#sec[$3$]]$ evaluates to $#lval[$4$][$#lH$]$,
+whereas $#suc[$3$]$ evaluates to $#lval[$4$][$#lL$]$.
+Similarly, #rel("B-Pred") evaluates $#prd[$e$]$ to $#lval[$i - 1$][$ell$]$ if $e$ evaluates to $#lval[$i$][$ell$]$.
+
+In summary, under these semantics, there is no expression an attacker
+can write that produces an $#lL$-labeled value
+whose content depends on any $#lH$-labeled (secret) input.
+The join in the conditional rules ensures that even _implicit_ information flows
+through branch selection are tracked and labeled private.