diff --git a/README.md b/README.md index 6c4a874..71f701d 100644 --- a/README.md +++ b/README.md @@ -192,7 +192,7 @@ There are three top-level modules in the [`src/`](./src) directory: $\Sigma$ is the heap context and $\mu$ is the (well-typed) heap. -### Technical definitions of the surface language $\lambda_{\mathtt{SEC}}^\star$ in `Surface/` +### Technical definitions of the surface language $\lambda_{\mathtt{SEC}}^\star$ [in directory `Surface/`](./src/Surface) - [`Surface.SurfaceSyntax`](./src/Surface/SurfaceSyntax.agda): The syntax definition of $\lambda_{\mathtt{SEC}}^\star$. It uses [the Abstract Binding Tree (ABT) library](https://github.com/jsiek/abstract-binding-trees). For example, the term of function @@ -207,7 +207,7 @@ There are three top-level modules in the [`src/`](./src) directory: language program, and $A$ is the security type that $M$ is typed at. -### Technical definitions of the cast calculus $\lambda_{\mathtt{SEC}}^{c}$ in `CC/` +### Technical definitions of the cast calculus $\lambda_{\mathtt{SEC}}^{c}$ [in directory `CC/`](./src/CC) - [`CC.CCSyntax`](./src/CC/CCSyntax.agda): The syntax definition of $\lambda_{\mathtt{SEC}}^{c}$. Again, the module uses the ABT library. There are a few terms that arise during runtime, including @@ -263,12 +263,46 @@ following auxiliary definitions: - [`CC.BigStepErased`](./src/CC/BigStepErased.agda): The big-step semantics for erased $\lambda_{\mathtt{SEC}}^{c}$. -### Technical definitions of the surface language $\lambda_{\mathtt{IFC}}^\star$ in `Surface2/` +### Technical definitions of the surface language $\lambda_{\mathtt{IFC}}^\star$ [in directory `Surface2/`](./src/Surface2) +- [`Surface2.Syntax`](./src/Surface2/Syntax.agda): The syntax of $\lambda_{\mathtt{IFC}}^\star$. The most noteworthy difference + from $\lambda_{\mathtt{SEC}}^\star$ is that in $\lambda_{\mathtt{IFC}}^\star$, the PC annotation on a $\lambda$ + is treated as a type annotation, which means that it can be $\star$. +- [`Surface2.Typing`](./src/Surface2/Typing.agda): The typing rules for $\lambda_{\mathtt{IFC}}^\star$. +- [`Surface2.Precision`](./src/Surface2/Precision.agda): The precision rules for $\lambda_{\mathtt{IFC}}^\star$. The precision + relation is used in the definition and the proof of the gradual guarantee. -### Technical definitions of the cast calculus $\lambda_{\mathtt{IFC}}^{c}$ in `CC2/` -- The coercion calculus for security labels +### The coercion calculus for security labels [in directory `CoercionExpr`](./src/CoercionExpr) -- Security label expressions that represent PC + +### Security label expressions [in directory `LabelExpr`](./src/LabelExpr) + + +### Technical definitions of the cast calculus $\lambda_{\mathtt{IFC}}^{c}$ [in directory `CC2/`](./src/CC2) + +- [`CC2.Syntax`](./src/CC2/Syntax.agda): As usual, the cast calculus $\lambda_{\mathtt{IFC}}^{c}$ is a statically-typed + language that includes an explicit term for casts. Many of the operators in + $\lambda_{\mathtt{IFC}}^{c}$ have two variants, a "static" one for when the pertinent security + label is statically known (such as `ref`) and the "dynamic" one for when the + security label is statically unknown (such as `ref?`). The operational + semantics of the "dynamic" variants involve runtime checking. +- [`CC2.Typing`](./src/CC2/Typing.agda): The typing judgment is of form + $\Gamma ; \Sigma ; g ; \ell \vdash M \Leftarrow A$. The six fields are of the + same meanings as those of $\lambda_{\mathtt{SEC}}^{c}$. The main difference is that the typing + of $\lambda_{\mathtt{IFC}}^{c}$ stays in checking mode, so the type $A$ is considered an input of + the judgment. +- [`CC2.HeapTyping`](./src/CC2/HeapTyping.agda): Lemmas about heap + well-typedness for $\lambda_{\mathtt{IFC}}^{c}$. They are similar to those of $\lambda_{\mathtt{SEC}}^{c}$ because + $\lambda_{\mathtt{IFC}}^{c}$ shares the same heap model as $\lambda_{\mathtt{SEC}}^{c}$. +- [`CC2.Values`](./src/CC2/Values.agda): The definition of values in $\lambda_{\mathtt{IFC}}^{c}$. + A raw value can be (1) a constant (2) an address or (3) a $\lambda$ + abstraction. A value can be either a raw value, or a raw value wrapped with an + irreducible cast. A cast is irreducible if its top-level security label + coercion is in normal form and the cast is not identity. +- [`CC2.Reduction`](./src/CC2/Reduction.agda): The operational semantics for $\lambda_{\mathtt{IFC}}^{c}$. Similar to the one of + $\lambda_{\mathtt{SEC}}^{c}$, the relation $M \mid \mu \mid \ell \longrightarrow N \mid \mu'$ + says that $\lambda_{\mathtt{IFC}}^{c}$ term $M$ reduces with heap $\mu$ under PC label $\ell$ to + term $N$ and heap $\mu'$. +- [`Compile.Compile`](./src/Compile/Compile.agda): The compilation function from $\lambda_{\mathtt{IFC}}^\star$ to $\lambda_{\mathtt{IFC}}^{c}$. diff --git a/README.org b/README.org index 6021c82..62bc84b 100644 --- a/README.org +++ b/README.org @@ -189,7 +189,7 @@ There are three top-level modules in the [[./src][=src/=]] directory: point-wise. The typing judgment has the form $\Sigma \vdash \mu$, where $\Sigma$ is the heap context and $\mu$ is the (well-typed) heap. -*** Technical definitions of the surface language {{{surface_old}}} in =Surface/= +*** Technical definitions of the surface language {{{surface_old}}} [[./src/Surface][in directory =Surface/=]] + [[./src/Surface/SurfaceSyntax.agda][=Surface.SurfaceSyntax=]]: The syntax definition of {{{surface_old}}}. It uses [[https://github.com/jsiek/abstract-binding-trees][the Abstract Binding Tree (ABT) library]]. For example, the term of function @@ -203,7 +203,7 @@ There are three top-level modules in the [[./src][=src/=]] directory: typing context, $g$ is the static program counter (PC) label, $M$ is a surface language program, and $A$ is the security type that $M$ is typed at. -*** Technical definitions of the cast calculus {{{cc_old}}} in =CC/= +*** Technical definitions of the cast calculus {{{cc_old}}} [[./src/CC][in directory =CC/=]] + [[./src/CC/CCSyntax.agda][=CC.CCSyntax=]]: The syntax definition of {{{cc_old}}}. Again, the module uses the ABT library. There are a few terms that arise during runtime, including @@ -257,10 +257,43 @@ following auxiliary definitions: of high security and thus appear to be opaque for a low observer. + [[./src/CC/BigStepErased.agda][=CC.BigStepErased=]]: The big-step semantics for erased {{{cc_old}}}. -*** Technical definitions of the surface language {{{surface}}} in =Surface2/= - -*** Technical definitions of the cast calculus {{{cc}}} in =CC2/= - -**** The coercion calculus for security labels - -**** Security label expressions that represent PC +*** Technical definitions of the surface language {{{surface}}} [[./src/Surface2][in directory =Surface2/=]] + ++ [[./src/Surface2/Syntax.agda][=Surface2.Syntax=]]: The syntax of {{{surface}}}. The most noteworthy difference + from {{{surface_old}}} is that in {{{surface}}}, the PC annotation on a $\lambda$ + is treated as a type annotation, which means that it can be $\star$. ++ [[./src/Surface2/Typing.agda][=Surface2.Typing=]]: The typing rules for {{{surface}}}. ++ [[./src/Surface2/Precision.agda][=Surface2.Precision=]]: The precision rules for {{{surface}}}. The precision + relation is used in the definition and the proof of the gradual guarantee. + +*** The coercion calculus for security labels [[./src/CoercionExpr][in directory =CoercionExpr=]] + +*** Security label expressions [[./src/LabelExpr][in directory =LabelExpr=]] + + +*** Technical definitions of the cast calculus {{{cc}}} [[./src/CC2][in directory =CC2/=]] + ++ [[./src/CC2/Syntax.agda][=CC2.Syntax=]]: As usual, the cast calculus {{{cc}}} is a statically-typed + language that includes an explicit term for casts. Many of the operators in + {{{cc}}} have two variants, a "static" one for when the pertinent security + label is statically known (such as ~ref~) and the "dynamic" one for when the + security label is statically unknown (such as ~ref?~). The operational + semantics of the "dynamic" variants involve runtime checking. ++ [[./src/CC2/Typing.agda][=CC2.Typing=]]: The typing judgment is of form + $\Gamma ; \Sigma ; g ; \ell \vdash M \Leftarrow A$. The six fields are of the + same meanings as those of {{{cc_old}}}. The main difference is that the typing + of {{{cc}}} stays in checking mode, so the type $A$ is considered an input of + the judgment. ++ [[./src/CC2/HeapTyping.agda][=CC2.HeapTyping=]]: Lemmas about heap + well-typedness for {{{cc}}}. They are similar to those of {{{cc_old}}} because + {{{cc}}} shares the same heap model as {{{cc_old}}}. ++ [[./src/CC2/Values.agda][=CC2.Values=]]: The definition of values in {{{cc}}}. + A raw value can be (1) a constant (2) an address or (3) a $\lambda$ + abstraction. A value can be either a raw value, or a raw value wrapped with an + irreducible cast. A cast is irreducible if its top-level security label + coercion is in normal form and the cast is not identity. ++ [[./src/CC2/Reduction.agda][=CC2.Reduction=]]: The operational semantics for {{{cc}}}. Similar to the one of + {{{cc_old}}}, the relation $M \mid \mu \mid \ell \longrightarrow N \mid \mu'$ + says that {{{cc}}} term $M$ reduces with heap $\mu$ under PC label $\ell$ to + term $N$ and heap $\mu'$. ++ [[./src/Compile/Compile.agda][=Compile.Compile=]]: The compilation function from {{{surface}}} to {{{cc}}}.