Sterling Example: simple_imp:security

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-ProjExpr]*
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-RFProj]*
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-Proj]*
secure PC G C G1