Extensibella Example: library:security

Language Specification

File: syntax.sos

[Reduce File] [Raw File] 
Module library:security

Builds on library:host

s ::= ...
    | secdecl(string, ty, sl, e)

sl ::= public
     | private

Projection sl :


---------------------------------------------- [P-secdecl]
|{s}- secdecl(N, Ty, Sl, E) ~~> decl(N, Ty, E)

File: typing.sos

[Reduce File] [Raw File] 
Module library:security

ty_e G E Ty
no_lookup G N
--------------------------------------- [TS-secdecl]
ty_s G secdecl(N, Ty, Sl, E) (N, Ty)::G

File: eval.sos

[Reduce File] [Raw File] 
Module library:security

eval_e G E V
---------------------------------------- [X-secdecl]
eval_s G secdecl(N, Ty, Sl, E) (N, V)::G

File: security.sos

[Reduce File] [Raw File] 
Module library:security

/*We use the standard library's lookup relation rather than writing
  our own here.*/

Fixed Judgment join : sl sl sl
/*Sigma |- level e* sl*/
Judgment level : [(string, sl)] e* sl
/*Sigma sl |- secure s* Sigma*/
Judgment secure : [(string, sl)] sl s* [(string, sl)]

========================= [J-public]
join public public public


====================== [J-private-l]
join private L private


====================== [J-private-r]
join L private private





------------------------- [L-int]
level SG intlit(I) public


--------------------- [L-true]
level SG trueE public


---------------------- [L-false]
level SG falseE public


lookup SG N L
----------------- [L-var]
level SG var(N) L


level SG E1 L1
level SG E2 L2
join L1 L2 L
---------------------- [L-add]
level SG add(E1, E2) L


level SG E1 L1
level SG E2 L2
join L1 L2 L
--------------------- [L-eq]
level SG eq(E1, E2) L


level SG E1 L1
level SG E2 L2
join L1 L2 L
--------------------- [L-gt]
level SG gt(E1, E2) L


level SG E L
----------------- [L-not]
level SG not(E) L


|{e}- E ~~> E1
level SG E1 Sl
-------------- [LF-level]*
level SG E Sl





--------------------- [S-skip]
secure SG Sl skipS SG


secure SG Sl S1 SG1
secure SG1 Sl S2 SG2
---------------------------- [S-seq]
secure SG Sl seq(S1, S2) SG2


level SG E public
no_lookup SG N
----------------------------------------------- [S-decl]
secure SG public decl(N, Ty, E) (N, public)::SG


level SG E L
lookup SG N private
---------------------------- [S-assign-private]
secure SG Sl assign(N, E) SG


level SG E public
lookup SG N public
-------------------------------- [S-assign-public]
secure SG public assign(N, E) SG


level SG E L
join L Sl Sl1
secure SG Sl1 S1 SG1
secure SG Sl1 S2 SG2
------------------------------- [S-ifte]
secure SG Sl ifte(E, S1, S2) SG


level SG E L
join L Sl Sl1
secure SG Sl1 S SG1
--------------------------- [S-while]
secure SG Sl while(E, S) SG


level SG E L
no_lookup SG N
-------------------------------------------------------- [S-secdecl-private]
secure SG Sl secdecl(N, Ty, private, E) (N, private)::SG


level SG E public
no_lookup SG N
---------------------------------------------------------- [S-secdecl-public]
secure SG public secdecl(N, Ty, public, E) (N, public)::SG


|{s}- S ~~> S1
secure SG Sl S1 SG1
------------------- [LF-secure]*
secure SG Sl S SG1

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module library:security.


Prove_Constraint library:host:proj_e_unique.
Prove_Constraint library:host:proj_e_is.


Prove_Constraint library:host:proj_s_unique. [Show Proof]

Prove_Constraint library:host:proj_s_is. [Show Proof]



Prove_Constraint library:host:proj_ty_unique.
Prove_Constraint library:host:proj_ty_is.


Add_Proj_Rel library:host:is_e.


Prove_Ext_Ind library:host:is_e.


Prove library:host:is_e_var_or_not.
Prove library:host:is_e_intlit_or_not.
Prove library:host:is_e_trueE_or_not.
Prove library:host:is_e_falseE_or_not.
Prove library:host:is_e_add_or_not.
Prove library:host:is_e_eqC_or_not.
Prove library:host:is_e_gt_or_not.
Prove library:host:is_e_not_or_not.
Prove library:host:is_e_eq_or_not.
Prove library:host:vars_unique.


Prove_Constraint library:host:proj_e_vars_exist.
Prove_Constraint library:host:proj_e_vars.


Prove library:host:vars_is.
Prove library:host:vars_exist.


Prove library:host:value_empty_typable.


Prove library:host:eval_e_is.

Prove library:host:type_preservation_e.

Prove library:host:var_types_maintained. [Show Proof]


Prove library:host:type_preservation_s. [Show Proof]



Prove_Constraint library:host:proj_eval_e.


Prove library:host:eval_e_unique.


Prove_Constraint library:host:proj_s_eval. [Show Proof]



Add_Ext_Size library:host:eval_s.
Add_Proj_Rel library:host:eval_s.


Prove_Ext_Ind library:host:eval_s. [Show Proof]


Prove_Constraint library:host:proj_s_eval_results. [Show Proof]



Prove_Constraint library:host:proj_s_eval_results_back. [Show Proof]



Prove library:host:eval_e_value.


Prove library:host:eval_s_value. [Show Proof]



Prove library:host:vars_eval_same_result.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                         SECURITY THEOREMS                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%because we don't have fixed types in Sterling, we make our own by
%adding this property
Extensible_Theorem
  sl_form : forall SL,
    Is : is_sl SL ->
    SL = public \/ SL = private
  on Is. [Show Proof]



Theorem join_unique : forall A B S1 S2,
  join A B S1 -> join A B S2 -> S1 = S2. [Show Proof]


Theorem join_public : forall A B,
  join A B public -> A = public /\ B = public. [Show Proof]



Extensible_Theorem
  level_public_vars : forall SG E V X,
    Lev : level SG E public ->
    Vars : vars E V ->
    Mem : mem X V ->
    lookup SG X public
  on Lev. [Show Proof]



Define public_equiv :
  list (pair string sl) -> list (pair string e) ->
  list (pair string e) -> prop by
public_equiv S G1 G2 :=
  (forall X V,
      lookup S X public ->
      lookup G1 X V -> lookup G2 X V) /\
  (forall X V,
      lookup S X public ->
      lookup G2 X V -> lookup G1 X V).

Theorem public_equiv_trans : forall SG GA GB GC,
  public_equiv SG GA GB -> public_equiv SG GB GC ->
  public_equiv SG GA GC. [Show Proof]



Theorem public_equiv_symm : forall SG GA GB,
  public_equiv SG GA GB -> public_equiv SG GB GA. [Show Proof]



Theorem public_equiv_refl : forall SG G,
  public_equiv SG G G. [Show Proof]



Theorem level_secure : forall SG G1 G2 E V1 V2,
  is_e E -> level SG E public -> public_equiv SG G1 G2 ->
  eval_e G1 E V1 -> eval_e G2 E V2 ->
  V1 = V2. [Show Proof]



Extensible_Theorem
  level_unique : forall SG E S1 S2,
    LevA : level SG E S1 ->
    LevB : level SG E S2 ->
    S1 = S2
  on LevA. [Show Proof]



Theorem level_not_public : forall SG G1 G2 E V1 V2,
  is_e E -> public_equiv SG G1 G2 -> level SG E public ->
  eval_e G1 E V1 -> eval_e G2 E V2 -> (V1 = V2 -> false) ->
  false. [Show Proof]



Extensible_Theorem
  stmt_public_branch : forall SG SL SG2 S X,
    Sec : secure SG SL S SG2 ->
    LkpSec : lookup SG X public ->
    lookup SG2 X public
  on Sec. [Show Proof]



Theorem public_equiv_swap : forall SG SG' GA GB,
  (forall X, lookup SG X public -> lookup SG' X public) ->
  public_equiv SG' GA GB -> public_equiv SG GA GB. [Show Proof]



Extensible_Theorem
  stmt_not_public_no_public_change : forall S SG SL SG1 G G1,
    Sec : secure SG SL S SG1 ->
    NEq : (SL = public -> false) ->
    Ev : eval_s G S G1 ->
    public_equiv SG G G1
  on Ev. [Show Proof]



Theorem while_no_public_change : forall SG SL SG' Cond Body S G G2,
  secure SG SL (while Cond Body) SG' -> level SG Cond S ->
  (S = public -> false) -> eval_s G (while Cond Body) G2 ->
  public_equiv SG G G2. [Show Proof]



Extensible_Theorem
  stmt_secure : forall S SG SL SG1 GA GA' GB GB',
    Is : is_s S ->
    Sec : secure SG SL S SG1 ->
    Rel : public_equiv SG GA GB ->
    EvA : eval_s GA S GA' ->
    EvB : eval_s GB S GB' ->
    public_equiv SG1 GA' GB'
  on EvA. [Show Proof]
Back to example home