Sterling Example: functions:security

File: security.sos

[Reduce File] [Raw File]

Module functions:security

Builds on functions:host

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


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


/*New way to declare function parameters*/
params ::= ...
         | addSecParams(string, seclevel, ty, params)


------------------------------------------- [Proj-AddSecParams]
|{params}- addSecParams(X, S, Ty, Rest) ~~>
           addParams(X, Ty, Rest)


/*New way to declare a function, with a minimum program counter to 
  start checking*/
fun ::= ...
      | secfun(string, seclevel, ty, seclevel, string, params, c)

------------------------------------------------------- [Proj-Secfun]
|{fun}- secfun(Name, Sec, RetTy, RetSec, RetName, Params, Body) ~~>
        fun(Name, RetTy, RetName, Params, Body)


seclevel ::= public | private
Projection seclevel :




/*Typing and Evaluation for New Statement*/

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


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



/*Host Relations for New Parameter*/

paramsToTyList Rest TRest
----------------------------------------------------- [PtTL-AddSec]
paramsToTyList addSecParams(X, S, Ty, Rest) Ty::TRest


paramsToTyCtx Rest TRest
--------------------------------------------------------- [PtTC-AddSec]
paramsToTyCtx addSecParams(X, S, Ty, Rest) (X, Ty)::TRest


paramsToNameList Rest NRest
------------------------------------------------------ [PtNL-AddSec]
paramsToNameList addSecParams(X, S, Ty, Rest) X::NRest



/*Host Relations for New Fun*/

paramsToTyCtx Params G
typeOK FG (RetName, RetTy)::G Body G2 /*ret name declared*/
------------------------------------------------------------ [T-Secfun]
funTyOK FG secfun(Name, Level, RetTy, RetSec, RetName, Params, Body)


paramsToTyList Params ArgTys
--------------------------------------------------------- [GFT-Secfun]
getFunTy secfun(Name, Level, RetTy, RetSec, RetName, Params, Body
               ) Name RetTy ArgTys


paramsToNameList Params Names
--------------------------------------------------------- [EF-Secfun]
{eval_fun secfun(Name, Level, RetTy, RetSec, RetName, Params, Body)
                  Name RetName Names Body}

File: analysis.sos

[Reduce File] [Raw File]

Module functions:security

funsecctx ::= emptyFunSec
      | addFunSec(string, seclevel, seclevel, [seclevel], funsecctx)
           /*name, starting PC, return level, param sec levels, rest*/
Projection funsecctx :


Judgment lookupFunSec : funsecctx* string seclevel seclevel [seclevel]

-------------------------------------------------------- [LFS-Here]
lookupFunSec addFunSec(X, S, RetS, SL, Rest) X S RetS SL


lookupFunSec Rest X XS XRet XSL
X != Y
---------------------------------------------------------- [LFS-Later]
lookupFunSec addFunSec(Y, YS, YRet, YSL, Rest) X XS XRet XSL


Judgment paramsToSecList : params* [seclevel]

---------------------------- [PtSL-End]
paramsToSecList endParams []


paramsToSecList Rest SRest
---------------------------------------------------- [PtSL-Add]
paramsToSecList addParams(X, Ty, Rest) public::SRest


paramsToSecList Rest SRest
----------------------------------------------------- [PtSL-AddSec]
paramsToSecList addSecParams(X, S, Ty, Rest) S::SRest


|{params}- P ~~> PT
paramsToSecList PT S
-------------------- [PtSL-D]*
paramsToSecList P S




/*Take two security levels and the 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




/*Expressions*/
Judgment level : seclevel funsecctx [(string, seclevel)] e* seclevel
Judgment rf_level : seclevel funsecctx [(string, seclevel)] recFieldExprs* seclevel
Judgment level_args : seclevel funsecctx [(string, seclevel)] args* [seclevel]
/*Statements*/
Judgment secure : seclevel funsecctx [(string, seclevel)] c* [(string, seclevel)]
/*Functions*/
Judgment secure_fun : funsecctx fun*
Judgment paramsToSecCtx : params* [(string, seclevel)]
/*Program*/
Judgment secure_program : funsecctx program*
Judgment buildFunSecCtx : program* funsecctx
Judgment getFunSec : fun* string seclevel seclevel [seclevel]
                /*name, starting level, return level, arg sec levels*/
/*The actual check for the program*/
Fixed Judgment programSecCheck : program


/*Expression Security Level*/

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


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


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


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


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


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


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


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


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


lookupFunSec FG Fun private RetLev Levels
level_args PC FG G Args Levels
----------------------------------------- [S-CallPrivate]
level PC FG G call(Fun, Args) RetLev
/*can always call a function starting in a private state*/


lookupFunSec FG Fun public RetLev Levels
level_args PC FG G Args Levels
---------------------------------------- [S-CallPublic]
level public FG G call(Fun, Args) RetLev
/*can only call a function starting in a public state if we are also
  in a public state (didn't branch on private vars)*/


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


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


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



/*Record Field Security Level*/

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


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


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



/*Argument Security Levels*/

----------------------------- [LA-End]
level_args PC FG G endArgs []


level PC FG G E S
level_args PC FG G Rest SRest
-------------------------------------------- [LA-Add]
level_args PC FG G addArgs(E, Rest) S::SRest


|{args}- A ~~> AT
level_args PC FG G AT S
----------------------- [LA-D]*
level_args PC FG G A S



/*Statement Security*/

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


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


level PC FG G E public
----------------------------------------------- [S-Declare]
secure PC FG G declare(X, Ty, E) (X, public)::G


level PC FG G E S
--------------------------------------------- [S-DeclareSecPrivate]
{secure PC FG G declareSec(X, private, Ty, E)
             (X, private)::G}


level PC FG G E public
------------------------------------------------ [S-DeclareSecPublic]
{secure public FG G declareSec(X, public, Ty, E)
                   (X, public)::G}


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


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


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


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


level PC FG G E public
-------------------------------- [S-Print]
secure public FG G printVal(E) G
/*can only print public values, and can only print if we didn't use
  private variables to get here*/


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



/*Function Security*/

paramsToSecCtx Params G
secure public FG G Body G2
----------------------------------------------------- [SF-Fun]
secure_fun FG fun(Name, RetTy, RetName, Params, Body)


paramsToSecCtx Params G
secure PC FG (RetName, RetSec)::G Body G2
------------------------------------------------------ [SF-Secfun]
secure_fun FG secfun(Name, PC, RetTy, RetSec, RetName,
                     Params, Body)


|{fun}- F ~~> FT
secure_fun FG FT
---------------- [SF-D]*
secure_fun FG F



--------------------------- [PtSC-End]
paramsToSecCtx endParams []


paramsToSecCtx Rest SRest
-------------------------------------------------------- [PtSC-Add]
paramsToSecCtx addParams(X, Ty, Rest) (X, public)::SRest


paramsToSecCtx Rest SRest
--------------------------------------------------------- [PtSC-AddSec]
paramsToSecCtx addSecParams(X, S, Ty, Rest) (X, S)::SRest


|{params}- P ~~> PT
paramsToSecCtx PT S
------------------- [PtSC-D]*
paramsToSecCtx P S



/*Program Security*/

---------------------------- [SP-End]
secure_program FG endProgram


secure_fun FG Fun
secure_program FG Rest
--------------------------------------- [SP-Add]
secure_program FG addProgram(Fun, Rest)


|{program}- P ~~> PT
secure_program FG PT
-------------------- [SP-D]*
secure_program FG P



------------------------------------- [BFSC-End]
buildFunSecCtx endProgram emptyFunSec


buildFunSecCtx Rest SRest
getFunSec Fun Name Lev RetLev Secs
----------------------------------------------------------- [BFSC-Add]
buildFunSecCtx addProgram(Fun, Rest
                  ) addFunSec(Name, Lev, RetLev, Secs, SRest)


|{program}- P ~~> PT
buildFunSecCtx PT GS
-------------------- [BFSC-D]*
buildFunSecCtx P GS



paramsToSecList Params SL
------------------------------------------------ [GFS-Fun]
getFunSec fun(Name, RetTy, RetName, Params, Body
             ) Name public public SL


paramsToSecList Params SL
--------------------------------------------------------- [GFS-Secfun]
getFunSec secfun(Name, S, RetTy, RetSec, RetName, Params, Body
                ) Name S RetSec SL


|{fun}- F ~~> FT
getFunSec FT Name S Ret SL
-------------------------- [GFS-D]*
getFunSec F Name S Ret SL



buildFunSecCtx P FG
secure_program FG P
=================== [PSecCheck]
programSecCheck P