diff --git a/semantics-1/semantics-typst.pdf b/semantics-1/semantics-typst.pdf index ba0ba42..f65700e 100644 Binary files a/semantics-1/semantics-typst.pdf and b/semantics-1/semantics-typst.pdf differ diff --git a/semantics-1/semantics.typ b/semantics-1/semantics.typ index 928113f..fb6159a 100644 --- a/semantics-1/semantics.typ +++ b/semantics-1/semantics.typ @@ -1,12 +1,7 @@ // ============================================================ // Operational Semantics for BoolInt* Language — Typst version // ============================================================ - -// ----- page setup (fullpage equivalent) --------------------- -#set page(margin: 1in) -#set text(size: 11pt) -#set par(justify: true) - +// // ----- helper functions ------------------------------------- // Language keywords rendered in monospace @@ -63,104 +58,6 @@ ) } -// ----- title block ------------------------------------------ - -#align(center)[ - #text(size: 17pt, weight: "bold")[Operational Semantics for BoolInt\* Language] - - #v(0.8em) - - Yuri Tatishchev \ - San José State University \ - iurii.tatishchev\@sjsu.edu -] - -#v(1em) - -// ----- abstract --------------------------------------------- - -#align(center)[ - #block(width: 85%)[ - #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. - ] -] - -#v(0.5em) - -// ----- body text -------------------------------------------- - -BoolInt\* is a very minimal language that allows us to experiment with operational semantics. - -First, we define the valid expressions in our language. -These expressions dictate the possibilities of what expressions -we may have in our source programs. -(Note that other language might also have _statements_. -Statements might not evaluate to a value; -expressions always will.) - -// ----- Figure 1: language definition ------------------------ - -#figure( - box(width: 85%, inset: (left: 2em))[ - #set align(left) - #mydefhead[$e ::=$ #h(6em)][Expressions] - #mydefcase(tr, [true value]) - #mydefcase(fl, [false value]) - #mydefcase($i$, [integers]) - #mydefcase(ife[$e$][$e$][$e$], [conditional expressions]) - #mydefcase(suc[$e$], [successor]) - #mydefcase(prd[$e$], [predecessor]) - #mydefcase(sec[$e$], [secret]) - - #v(0.5em) - - #mydefhead[$v ::=$ #h(6em)][Values] - #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 with security labels], -) - -@fig:lang shows the list of expressions, values, and security labels for the BoolInt\* language. -Expressions can be the value $#tr$, the value $#fl$, -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 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$][$#lval[$v$][$ell$]$] $ - -The above line should be read as -"the expression $e$ evaluates to the value $v$ with security label $ell$". // ----- Figure 2: big-step semantics ------------------------- @@ -171,7 +68,7 @@ The above line should be read as #v(0.6em) - #bsrule("B-Value", $emptyset$, $#bstep[$v$][$#lval[$v$][$#lL$]$]$) + #bsrule("B-Value", "", $#bstep[$v$][$#lval[$v$][$#lL$]$]$) #bsrule("B-Secret", $#bstep[$e$][$#lval[$v$][$ell$]$]$, $#bstep[#sec[$e$]][$#lval[$v$][$#lH$]$]$) @@ -193,50 +90,3 @@ The above line should be read as ], caption: [Big-step semantics for BoolInt\* with information flow], ) - -@fig:bigstep shows the big-step evaluation rules for the BoolInt\* language -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 bare value evaluates to itself with a public label $#lL$, -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 $#lval[$#tr$][$ell_1$]$ -and $e_2$ evaluates to $#lval[$v$][$ell_2$]$. -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 $#lval[$i$][$ell$]$, -then the expression $#suc[$e$]$ evaluates to $#lval[$i + 1$][$ell$]$. -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.