diff --git a/README.md b/README.md index 364f40c..876a4a9 100644 --- a/README.md +++ b/README.md @@ -98,26 +98,26 @@ A (fairly) large part of the code-base is shared between $\lambda_{\mathtt{IFC}} $\lambda_{\mathtt{SEC}}^\star$. -## Meta-theoretical results and demo programs +## Top-level modules of meta-theoretical results and demo programs There are three top-level modules in the [`src/`](./src) directory: -1. [**`Proofs`**](./src/Proofs.agda): sources the proofs of important **meta-theoretical results** - in the following modules: - - Here are some meta-theoretical results for $\lambda_{\mathtt{SEC}}^\star$ and its cast - calculus $\lambda_{\mathtt{SEC}}^{c}$: +1. [**`Proofs`**](./src/Proofs.agda): The module sources the proofs of important **meta-theoretical + results** in the following files: + - Meta-theoretical results for $\lambda_{\mathtt{SEC}}^\star$ and its cast calculus + $\lambda_{\mathtt{SEC}}^{c}$: - [`CC.TypeSafety`](./src/CC/TypeSafety.agda): $\lambda_{\mathtt{SEC}}^{c}$ is type safe by satisfying progress and preservation. - [`CC.BigStepPreservation`](./src/CC/BigStepPreservation.agda): The big-step semantics of $\lambda_{\mathtt{SEC}}^{c}$ also - preserves types. The big-step semantics + preserves types. This big-step semantics is used in the erasure-based + noninterference proof. - [`CC.BigStepErasedDeterministic`](./src/CC/BigStepErasedDeterministic.agda): The big-step evaluation of erased $\lambda_{\mathtt{SEC}}^{c}$ is deterministic. - [`CC.Noninterference`](./src/CC/Noninterference.agda): $\lambda_{\mathtt{SEC}}^{c}$ satisfies termination-insensitive noninterference (TINI). - [`CC.Compile`](./src/CC/Compile.agda): The compilation from $\lambda_{\mathtt{SEC}}^\star$ to $\lambda_{\mathtt{SEC}}^{c}$ preserves types. - - Here are meta-theoretical results for $\lambda_{\mathtt{IFC}}^\star$ and its cast calculus - $\lambda_{\mathtt{IFC}}^{c}$: + - Meta-theoretical results for $\lambda_{\mathtt{IFC}}^\star$ and its cast calculus $\lambda_{\mathtt{IFC}}^{c}$: - [`CC2.Progress`](./src/CC2/Progress.agda): $\lambda_{\mathtt{IFC}}^{c}$ satisfies progress, so that a well-typed $\lambda_{\mathtt{IFC}}^{c}$ term is either a value or a blame, which does not reduce, or the term takes one reduction step. @@ -172,14 +172,14 @@ There are three top-level modules in the [`src/`](./src) directory: blame, that contains its blame label. In this way, the programmer knows which cast is causing the problem. - [`Common.TypeBasedCast`](./src/Common/TypeBasedCast.agda): This module defines *type-based casts* between two - security types. In particular, $\lambda_{\mathtt{SEC}}^{c}$ uses type-based cast as its + security types. In particular, $\lambda_{\mathtt{SEC}}^{c}$ uses type-based casts as its cast representation. - [`Common.Coercions`](./src/Common/Coercions.agda): This modules defines the coercion-based cast - representation used by $\lambda_{\mathtt{IFC}}^{c}$; in particular, it defines the *security + representation used by $\lambda_{\mathtt{IFC}}^{c}$. In particular, it defines the *security coercions on values* of $\lambda_{\mathtt{IFC}}^{c}$. -### The shared heap model [in directory `Memory/`](./src/Memory) +### The heap model of $\lambda_{\mathtt{SEC}}^\star$ and $\lambda_{\mathtt{IFC}}^\star$ [in directory `Memory/`](./src/Memory) - [`Memory.Addr`](./src/Memory/Addr.agda): Definition of memory addresses. - [`Memory.Heap`](./src/Memory/Heap.agda): Definition and helper methods of the split-heap model, where @@ -224,9 +224,9 @@ There are three top-level modules in the [`src/`](./src) directory: - [`CC.Values`](./src/CC/Values.agda): The definition of values in $\lambda_{\mathtt{SEC}}^{c}$. A value can be (1) a constant (2) an address (3) a $\lambda$ abstraction or (4) a value wrapped with an irreducible (`Inert`) cast. The opaque term is also a value in the - semantics of erased $\lambda_{\mathtt{SEC}}^{c}$. There are canonical-form lemmas for - constants, functions, and memory addresses in this model: for example, a value - of function type must be either a $\lambda$ or a function proxy (a $\lambda$ + semantics of erased $\lambda_{\mathtt{SEC}}^{c}$. In this module, there are canonical-form + lemmas for constants, functions, and memory addresses. For example, a value of + function type must be either a $\lambda$ or a function proxy (a $\lambda$ wrapped with at least one inert function cast). - [`CC.Reduction`](./src/CC/Reduction.agda): The operational semantics for $\lambda_{\mathtt{SEC}}^{c}$. The relation $M \mid \mu \mid \ell \longrightarrow N \mid \mu'$ says that $\lambda_{\mathtt{SEC}}^{c}$ @@ -248,26 +248,29 @@ There are three top-level modules in the [`src/`](./src) directory: - [`CC.Interp`](./src/CC/Interp.agda): A stepper that replies on the progress proof to generate a reduction sequence of $k$ steps for a well-typed $\lambda_{\mathtt{SEC}}^{c}$ term. - [`CC.Compile`](./src/CC/Compile.agda): Compilation from $\lambda_{\mathtt{SEC}}^\star$ to $\lambda_{\mathtt{SEC}}^{c}$. The module - also contains a proof that the compilation preserves types + also contains a proof that this compilation function preserves types (`compilation-preserves-type`). The noninterference proof of $\lambda_{\mathtt{SEC}}^{c}$ is erasure-based. It uses the following auxiliary definitions: - [`CC.BigStep`](./src/CC/BigStep.agda): The big-step semantics for $\lambda_{\mathtt{SEC}}^{c}$. It is a direct - mechanical translation from the semantics in [CC.Reduction](./src/CC/Reduction.agda). -- [`CC.Erasure`](./src/CC/Erasure.agda): Definition of the erasure functions for $\lambda_{\mathtt{SEC}}^{c}$ terms - (`erase`) and heaps (`erase-μ`). Note that the memory cells of high security - are completely erased, because the values read from those cells are always - of high security and thus appear to be opaque for a low observer. + mechanical translation from the semantics in [`CC.Reduction`](./src/CC/Reduction.agda). +- [`CC.Erasure`](./src/CC/Erasure.agda): Definition of the erasure functions for terms (`erase`) and + heaps (`erase-μ`) in $\lambda_{\mathtt{SEC}}^{c}$. Note that the memory cells of high security + are completely erased, because the values read from those cells are always of + high security and thus appear to be opaque from a low-observer's point of + view. - [`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 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$. + from $\lambda_{\mathtt{SEC}}^\star$ is that in $\lambda_{\mathtt{IFC}}^\star$, the PC annotation on a + $\lambda$ is treated as a type annotation instead of a value annotation, which + means that it is allowed to be $\star$ in $\lambda_{\mathtt{IFC}}^\star$ (but not in + $\lambda_{\mathtt{SEC}}^\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. @@ -275,10 +278,10 @@ following auxiliary definitions: ### The coercion calculus for security labels [in directory `CoercionExpr/`](./src/CoercionExpr) -This directory contains the definition of and lemmas about the *coercion calculus -on security labels*. +This directory contains the definition of and the lemmas about the *coercion +calculus on security labels*. -- [`CoercionExpr.Coercions`](./src/CoercionExpr/Coercions.agda): One single coercion on security labels can either +- [`CoercionExpr.Coercions`](./src/CoercionExpr/Coercions.agda): A single coercion on security labels can either be identity ($\mathbf{id}$), subtype ($\uparrow$), injection from $\ell$ ($\ell!$), or projection to $\ell$ with blame label $p$ ($\ell?^p$). - [`CoercionExpr.CoercionExpr`](./src/CoercionExpr/CoercionExpr.agda): The syntax, typing, reduction, and normal forms diff --git a/README.org b/README.org index 04f9945..57c0d4c 100644 --- a/README.org +++ b/README.org @@ -99,26 +99,26 @@ All Agda source files are located in the [[./src][=src/=]] directory and end wit A (fairly) large part of the code-base is shared between {{{surface}}} and {{{surface_old}}}. -** Meta-theoretical results and demo programs +** Top-level modules of meta-theoretical results and demo programs There are three top-level modules in the [[./src][=src/=]] directory: -1. [[./src/Proofs.agda][*=Proofs=*]]: sources the proofs of important *meta-theoretical results* - in the following modules: - * Here are some meta-theoretical results for {{{surface_old}}} and its cast - calculus {{{cc_old}}}: +1. [[./src/Proofs.agda][*=Proofs=*]]: The module sources the proofs of important *meta-theoretical + results* in the following files: + * Meta-theoretical results for {{{surface_old}}} and its cast calculus + {{{cc_old}}}: * [[./src/CC/TypeSafety.agda][=CC.TypeSafety=]]: {{{cc_old}}} is type safe by satisfying progress and preservation. * [[./src/CC/BigStepPreservation.agda][=CC.BigStepPreservation=]]: The big-step semantics of {{{cc_old}}} also - preserves types. The big-step semantics + preserves types. This big-step semantics is used in the erasure-based + noninterference proof. * [[./src/CC/BigStepErasedDeterministic.agda][=CC.BigStepErasedDeterministic=]]: The big-step evaluation of erased {{{cc_old}}} is deterministic. * [[./src/CC/Noninterference.agda][=CC.Noninterference=]]: {{{cc_old}}} satisfies termination-insensitive noninterference (TINI). * [[./src/CC/Compile.agda][=CC.Compile=]]: The compilation from {{{surface_old}}} to {{{cc_old}}} preserves types. - * Here are meta-theoretical results for {{{surface}}} and its cast calculus - {{{cc}}}: + * Meta-theoretical results for {{{surface}}} and its cast calculus {{{cc}}}: * [[./src/CC2/Progress.agda][=CC2.Progress=]]: {{{cc}}} satisfies progress, so that a well-typed {{{cc}}} term is either a value or a blame, which does not reduce, or the term takes one reduction step. @@ -171,13 +171,13 @@ There are three top-level modules in the [[./src][=src/=]] directory: blame, that contains its blame label. In this way, the programmer knows which cast is causing the problem. + [[./src/Common/TypeBasedCast.agda][=Common.TypeBasedCast=]]: This module defines /type-based casts/ between two - security types. In particular, {{{cc_old}}} uses type-based cast as its + security types. In particular, {{{cc_old}}} uses type-based casts as its cast representation. + [[./src/Common/Coercions.agda][=Common.Coercions=]]: This modules defines the coercion-based cast - representation used by {{{cc}}}; in particular, it defines the /security + representation used by {{{cc}}}. In particular, it defines the /security coercions on values/ of {{{cc}}}. -*** The shared heap model [[./src/Memory][in directory =Memory/=]] +*** The heap model of {{{surface_old}}} and {{{surface}}} [[./src/Memory][in directory =Memory/=]] + [[./src/Memory/Addr.agda][=Memory.Addr=]]: Definition of memory addresses. + [[./src/Memory/Heap.agda][=Memory.Heap=]]: Definition and helper methods of the split-heap model, where @@ -220,9 +220,9 @@ There are three top-level modules in the [[./src][=src/=]] directory: + [[./src/CC/Values.agda][=CC.Values=]]: The definition of values in {{{cc_old}}}. A value can be (1) a constant (2) an address (3) a $\lambda$ abstraction or (4) a value wrapped with an irreducible (~Inert~) cast. The opaque term is also a value in the - semantics of erased {{{cc_old}}}. There are canonical-form lemmas for - constants, functions, and memory addresses in this model: for example, a value - of function type must be either a $\lambda$ or a function proxy (a $\lambda$ + semantics of erased {{{cc_old}}}. In this module, there are canonical-form + lemmas for constants, functions, and memory addresses. For example, a value of + function type must be either a $\lambda$ or a function proxy (a $\lambda$ wrapped with at least one inert function cast). + [[./src/CC/Reduction.agda][=CC.Reduction=]]: The operational semantics for {{{cc_old}}}. The relation $M \mid \mu \mid \ell \longrightarrow N \mid \mu'$ says that {{{cc_old}}} @@ -244,34 +244,37 @@ There are three top-level modules in the [[./src][=src/=]] directory: + [[./src/CC/Interp.agda][=CC.Interp=]]: A stepper that replies on the progress proof to generate a reduction sequence of $k$ steps for a well-typed {{{cc_old}}} term. + [[./src/CC/Compile.agda][=CC.Compile=]]: Compilation from {{{surface_old}}} to {{{cc_old}}}. The module - also contains a proof that the compilation preserves types + also contains a proof that this compilation function preserves types (~compilation-preserves-type~). The noninterference proof of {{{cc_old}}} is erasure-based. It uses the following auxiliary definitions: + [[./src/CC/BigStep.agda][=CC.BigStep=]]: The big-step semantics for {{{cc_old}}}. It is a direct - mechanical translation from the semantics in [[./src/CC/Reduction.agda][CC.Reduction]]. -+ [[./src/CC/Erasure.agda][=CC.Erasure=]]: Definition of the erasure functions for {{{cc_old}}} terms - (~erase~) and heaps (~erase-μ~). Note that the memory cells of high security - are completely erased, because the values read from those cells are always - of high security and thus appear to be opaque for a low observer. + mechanical translation from the semantics in [[./src/CC/Reduction.agda][=CC.Reduction=]]. ++ [[./src/CC/Erasure.agda][=CC.Erasure=]]: Definition of the erasure functions for terms (~erase~) and + heaps (~erase-μ~) in {{{cc_old}}}. Note that the memory cells of high security + are completely erased, because the values read from those cells are always of + high security and thus appear to be opaque from a low-observer's point of + view. + [[./src/CC/BigStepErased.agda][=CC.BigStepErased=]]: The big-step semantics for erased {{{cc_old}}}. *** 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$. + from {{{surface_old}}} is that in {{{surface}}}, the PC annotation on a + $\lambda$ is treated as a type annotation instead of a value annotation, which + means that it is allowed to be $\star$ in {{{surface}}} (but not in + {{{surface_old}}}). + [[./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/=]] -This directory contains the definition of and lemmas about the /coercion calculus -on security labels/. +This directory contains the definition of and the lemmas about the /coercion +calculus on security labels/. -+ [[./src/CoercionExpr/Coercions.agda][=CoercionExpr.Coercions=]]: One single coercion on security labels can either ++ [[./src/CoercionExpr/Coercions.agda][=CoercionExpr.Coercions=]]: A single coercion on security labels can either be identity ($\mathbf{id}$), subtype ($\uparrow$), injection from $\ell$ ($\ell!$), or projection to $\ell$ with blame label $p$ ($\ell?^p$). + [[./src/CoercionExpr/CoercionExpr.agda][=CoercionExpr.CoercionExpr=]]: The syntax, typing, reduction, and normal forms