Extensibella Example: simple_imp:security

Language Specification

File: security.sos

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

Builds on simple_imp:host

/*New Statement and Projection*/
c ::= ...
    | declareSec(string, seclevel, ty, e)


--------------------------------------------------- [Proj-DeclareSec]
|{c}- declareSec(X, S, Ty, E) ~~> declare(X, Ty, E)


seclevel ::= public | private
Projection seclevel :




/*Typing and Evaluation for New Statement*/

no_lookup G X /*still can't overwrite existing decls*/
typeOf G E Ty
------------------------------------------- [T-DeclareSec]
typeOK G declareSec(X, S, Ty, E) (X, Ty)::G


eval_e G E V
------------------------------------------ [E-DeclareSec]
eval_c G declareSec(X, S, Ty, E) (X, V)::G

File: analysis.sos

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

/*Take two security levels and then get the higher one*/
Judgment join : seclevel* seclevel seclevel

------------------------- [J-Publics]
join public public public


---------------------- [J-Private1]
join private S private


---------------------- [J-Private2]
join S private private




Judgment level : [(string, seclevel)] e* seclevel
Judgment rf_level : [(string, seclevel)] recFieldExprs* seclevel
Judgment secure : seclevel [(string, seclevel)] c* [(string, seclevel)]


/*Expression Security Level*/

--------------------- [S-Num]
level G num(I) public


level G E1 S1
level G E2 S2
join S1 S2 S
---------------------- [S-Plus]
level G plus(E1, E2) S


lookup G X S
----------------- [S-Name]
level G name(X) S


level G E1 S1
level G E2 S2
join S1 S2 S
------------------------- [S-Greater]
level G greater(E1, E2) S


level G E1 S1
level G E2 S2
join S1 S2 S
-------------------- [S-Eq]
level G eq(E1, E2) S


level G E1 S1
level G E2 S2
join S1 S2 S
--------------------- [S-And]
level G and(E1, E2) S


level G E1 S1
level G E2 S2
join S1 S2 S
-------------------- [S-Or]
level G or(E1, E2) S


------------------- [S-True]
level G true public


-------------------- [S-False]
level G false public


rf_level G Fields S
-------------------------- [S-RecBuild]
level G recBuild(Fields) S


level G Rec S
------------------------------------ [S-RecField]
level G recFieldAccess(Rec, Field) S


|{e}- E ~~> ET
level G ET S
-------------- [S-Expr-D]*
level G E S



/*Record Field Security Level*/

---------------------------------- [S-RFEnd]
rf_level G endRecFieldExprs public


level G E S1
rf_level G Rest S2
join S1 S2 S
----------------------------------------- [S-RFAdd]
rf_level G addRecFieldExprs(L, E, Rest) S


|{recFieldExprs}- RF ~~> RFT
rf_level G RFT S
---------------------------- [S-RF-D]*
rf_level G RF S



/*Statement Security*/

------------------ [S-Noop]
secure PC G noop G


secure PC G C1 G1
secure PC G1 C2 G2
-------------------------- [S-Seq]
secure PC G seq(C1, C2) G2


level G E public
no_lookup G X /*no previous assignment*/
------------------------------------------------ [S-Declare]
secure public G declare(X, Ty, E) (X, public)::G


level G E S
no_lookup G X /*no previous assignment*/
------------------------------------------ [S-DeclareSecPrivate]
{secure PC G declareSec(X, private, Ty, E)
        (X, private)::G}


level G E public
no_lookup G X /*no previous assignment*/
--------------------------------------------- [S-DeclareSecPublic]
{secure public G declareSec(X, public, Ty, E)
        (X, public)::G}


/*To assign to public var, need both PC and expr to be public*/
level G E public
lookup G X public
------------------------------ [S-AssignPublic]
secure public G assign(X, E) G


/*Can assign anything to a private var, anytime*/
level G E S
lookup G X private
-------------------------- [S-AssignPrivate]
secure PC G assign(X, E) G


/*Like assignment, since it is a version of it*/
level G E public
lookup G R public
------------------------------------ [S-RecUpdatePublic]
secure public G recUpdate(R, F, E) G


level G E S
lookup G R private
-------------------------------- [S-RecUpdatePrivate]
secure PC G recUpdate(R, F, E) G


level G Cond S
join PC S NewPC
secure NewPC G Then GTh
secure NewPC G Else GEl
------------------------------------------ [S-IfThenElse]
secure PC G ifThenElse(Cond, Then, Else) G
/*branches are new scopes, so we throw their security updates away*/


level G Cond S
join PC S NewPC
secure NewPC G Body G1
------------------------------- [S-While]
secure PC G while(Cond, Body) G
/*body is a new scope*/


|{c}- C ~~> CT
secure PC G CT G1
----------------- [S-D]*
secure PC G C G1

Reasoning

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

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

Module simple_imp:security.

Prove_Constraint simple_imp:host:proj_e_unique.
Prove_Constraint simple_imp:host:proj_e_is.
Prove_Constraint simple_imp:host:proj_rf_unique.
Prove_Constraint simple_imp:host:proj_rf_is.
Prove_Constraint simple_imp:host:proj_c_unique. [Show Proof]

Prove_Constraint simple_imp:host:proj_c_is. [Show Proof]

Prove_Constraint simple_imp:host:proj_recFields_unique.
Prove_Constraint simple_imp:host:proj_recFields_is.
Prove_Constraint simple_imp:host:proj_ty_unique.
Prove_Constraint simple_imp:host:proj_ty_is.
Prove_Constraint simple_imp:host:proj_value_unique.
Prove_Constraint simple_imp:host:proj_value_is.

Prove simple_imp:host:vars_join,
      simple_imp:host:vars_rf_join.

Prove simple_imp:host:vars_unique,
      simple_imp:host:vars_rf_unique.

Prove_Constraint simple_imp:host:proj_e_vars_exist.
Prove_Constraint simple_imp:host:proj_e_vars.
Prove_Constraint simple_imp:host:proj_rf_vars_exist.
Prove_Constraint simple_imp:host:proj_rf_vars.

Prove simple_imp:host:vars_is, simple_imp:host:vars_rf_is.
Prove simple_imp:host:vars_exist, simple_imp:host:vars_rf_exist.

Prove simple_imp:host:typeOf_unique, simple_imp:host:typeRecFields_unique.
Prove simple_imp:host:typeOK_unique. [Show Proof]


Prove_Constraint simple_imp:host:proj_eval_e.

Prove simple_imp:host:eval_e_unique,
      simple_imp:host:eval_rf_unique.

Prove simple_imp:host:update_rec_fields_unique.

Prove_Constraint simple_imp:host:proj_c_eval. [Show Proof]


Add_Ext_Size simple_imp:host:eval_c.
Add_Proj_Rel simple_imp:host:eval_c.

Prove_Ext_Ind simple_imp:host:eval_c. [Show Proof]


Prove simple_imp:host:eval_c_unique. [Show Proof]


Prove_Constraint simple_imp:host:proj_c_eval_results. [Show Proof]


Prove_Constraint simple_imp:host:proj_c_eval_results_back. [Show Proof]


Prove simple_imp:host:vars_eval_same_result,
      simple_imp:host:vars_equal_rf_same_result.



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

%We need this to make join_unique below possible
%Problem arises due to disallowed case analysis
Extensible_Theorem
  join_private_left : forall A S,
    Join : join A private S ->
    S = private
  on Join. [Show Proof]

Extensible_Theorem
  join_unique : forall A B S1 S2,
    J1 : join A B S1 ->
    J2 : join A B S2 ->
    S1 = S2
  on J1. [Show Proof]

Extensible_Theorem
  join_public : forall A B,
    J: join A B public ->
    A = public /\ B = public
  on J. [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,
  level_public_vars_rf : forall SG RF V X,
    Lev : rf_level SG RF public ->
    Vars : vars_rf RF V ->
    Mem : mem X V ->
    lookup SG X public
  on Lev. [Show Proof]



Define public_equiv :
  list (pair string seclevel) -> list (pair string value) ->
  list (pair string value) -> prop by
public_equiv S G1 G2 :=
  (forall X V1 V2,
      lookup S X public ->
      lookup G1 X V1 -> lookup G2 X V2 -> V1 = V2) /\
  (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,
  level_rf_unique : forall SG RF S1 S2,
    LevA : rf_level SG RF S1 ->
    LevB : rf_level SG RF 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 PC SG SG2 G G2 C X,
    Sec : secure PC SG C SG2 ->
    Ev : eval_c G C G2 ->
    LkpSec : lookup SG X public ->
    lookup SG2 X public
  on Ev. [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 C S SG SG1 G G1,
    Sec : secure S SG C SG1 ->
    NEq : (S = public -> false) ->
    Ev : eval_c G C G1 ->
    public_equiv SG G G1
  on Ev. [Show Proof]



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



Extensible_Theorem
  stmt_secure : forall C PC SG SG1 GA GA' GB GB',
    Is : is_c C ->
    Sec : secure PC SG C SG1 ->
    Rel : public_equiv SG GA GB ->
    EvA : eval_c GA C GA' ->
    EvB : eval_c GB C GB' ->
    public_equiv SG1 GA' GB'
  on EvA. [Show Proof]
Back to example home