Module exactEval:security
Builds on exactEval:host
stmt ::= ...
| secdecl(slev, typ, string, expr)
--------------------------------------- [Proj-Secdecl]
Names |{stmt}- secdecl(L, Ty, X, E) ~~>
declare(Ty, X, E)
fun ::= ...
/*secfun(name, ret ty, ret lev, ret var, init ret var val,
params, body)*/
| secfun(string, typ, slev, string, value, [param], stmt)
----------------------------------------------------- [Proj-SecFun]
|{fun}- secfun(Name, RetTy, RetLev, RetVar, RVVal,
Params, Body) ~~>
fun(Name, RetTy, RetVar, RVVal, Params, Body)
param ::= ...
| secparam(string, typ, slev)
--------------------------------------------------- [Proj-SecParam]
|{param}- secparam(Name, Ty, L) ~~> param(Name, Ty)
slev ::= private
| public
Projection slev :
exprNames Scope::Ctx E N
-------------------------------------------- [SN-Secdecl]
{stmtNames Scope::Ctx secdecl(L, Ty, X, E) N
(X::Scope)::Ctx}
no_lookup Scope X /*can't redeclare in scope*/
typeOf FC Scope::RestTC E Ty
--------------------------------------------- [T-Secdecl]
{stmtOK FC Scope::RestTC secdecl(L, Ty, X, E)
((X, Ty)::Scope)::RestTC}
/*check the function is well-typed with given types*/
paramTys Params ParamTys
stmtOK FC [(RetVar, RetTy)::ParamTys] Body FinalTC
/*check the function ctx contains the given types for this function*/
lookup FC FunName (RetTy, PTys)
values ParamTys PTys
/*no param with same name as return variable*/
no_lookup ParamTys RetVar
valueType RVVal RetTy
------------------------------------------------------ [T-SecFun]
funOK FC secfun(FunName, RetTy, RetLev, RetVar, RVVal,
Params, Body)
paramTys Params NameTys
values NameTys PTys
--------------------------------------------------------- [GFI-SecFun]
{getFunInfo secfun(FunName, RetTy, RetLev, RetVar, RVVal,
Params, Body) FunName RetTy PTys}
------------------------------------- [PT-SecParam]
paramTy secparam(Name, Ty, L) Name Ty
evalExpr FE EE E V Scope::EE1 O
---------------------------------------------------------- [E-Secdecl]
evalStmt FE EE secdecl(L, Ty, X, E) ((X, V)::Scope)::EE1 O
paramNames Params PNames
-------------------------------------------------------- [GFEI-SecFun]
{getFunEvalInfo secfun(FunName, RetTy, RetLev, RetVar,
RVVal, Params, Body)
FunName RetVar RVVal PNames Body}
------------------------------------ [PN-SecParam]
paramName secparam(Name, Ty, L) Name
Module exactEval:security /* The type [[(string, slev)]] is a set of scopes for security typing. As with typing and evaluation, the most recent scope is first. The type [(string, (slev, [slev]))] is the function context, listing the known functions with their return security slevs and argument security slevs. */ /*fun ctx, level ctx, program counter, expression, level*/ Judgment level : {[(string, (slev, [slev]))] [[(string, slev)]] slev expr* slev} Fixed Judgment levelArgs : { [(string, (slev, [slev]))] [[(string, slev)]] slev args [slev]} Fixed Judgment levelRecFields : { [(string, (slev, [slev]))] [[(string, slev)]] slev recFieldExprs slev} /*fun ctx, level ctx, programm counter, stmt, updated level ctx*/ Judgment secure : {[(string, (slev, [slev]))] [[(string, slev)]] slev stmt* [[(string, slev)]]} Judgment funSecure : [(string, (slev, [slev]))] fun* Fixed Judgment paramSecs : [param] [(string, slev)] Judgment paramSec : param* string slev Fixed Judgment funsSecure : [(string, (slev, [slev]))] [fun] Judgment getFunSec : fun* string slev [slev] Fixed Judgment gatherFunSecCtx : [fun] [(string, (slev, [slev]))] /*program, security levels of arguments to main*/ Judgment programSecure : program* [slev] /******************************************************************** Maximum of Security Levels ********************************************************************/ Judgment join : slev* slev slev ------------------------- [J-Public] join public public public ---------------------- [J-Private-L] join private L private ---------------------- [J-Private-R] join L private private /******************************************************************** Expression, Argument, and Record Field Levels ********************************************************************/ ---------------------------- [L-Num] level SF SG Sl num(I) public level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L ----------------------------- [L-Plus] level SF SG Sl plus(E1, E2) L level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L ------------------------------ [L-Minus] level SF SG Sl minus(E1, E2) L level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L ----------------------------- [L-Mult] level SF SG Sl mult(E1, E2) L level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L ---------------------------- [L-Div] level SF SG Sl div(E1, E2) L -------------------------- [L-True] level SF SG Sl true public --------------------------- [L-False] level SF SG Sl false public /*Because of short-circuiting evaluation, we need to treat and and or like ifThenElse, incorportaing the level of E1 into the PC of E2*/ level SF SG Sl E1 L1 join L1 Sl Sl1 level SF SG Sl1 E2 L2 join L1 L2 L ---------------------------- [L-And] level SF SG Sl and(E1, E2) L level SF SG Sl E1 L1 join L1 Sl Sl1 level SF SG Sl1 E2 L2 join L1 L2 L --------------------------- [L-Or] level SF SG Sl or(E1, E2) L level SF SG Sl E L ----------------------- [L-Not] level SF SG Sl not(E) L level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L -------------------------------- [L-Greater] level SF SG Sl greater(E1, E2) L level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L --------------------------- [L-Eq] level SF SG Sl eq(E1, E2) L ---------------------------------- [L-String] level SF SG Sl stringLit(S) public level SF SG Sl E1 L1 level SF SG Sl E2 L2 join L1 L2 L ---------------------------------- [L-AppString] level SF SG Sl appString(E1, E2) L lookupScopes X SG L ------------------------ [L-Name] level SF SG Sl name(X) L /*in private contexts, only private functions so we don't leak where we are by function output*/ lookup SF Fun (private, ArgLevs) levelArgs SF SG private Args ArgLevs ------------------------------------------- [L-Call-Private] level SF SG private call(Fun, Args) private lookup SF Fun (RetLev, ArgLevs) levelArgs SF SG public Args ArgLevs ----------------------------------------- [L-Call-Public] level SF SG public call(Fun, Args) RetLev secure SF []::SG Sl S SG1 level SF SG1 Sl E L ------------------------------- [L-StmtExpr] level SF SG Sl stmtExpr(S, E) L levelRecFields SF SG Sl Fields L --------------------------------- [L-RecBuild] level SF SG Sl recBuild(Fields) L level SF SG Sl E L ----------------------------------------- [L-RecAccess] level SF SG Sl recFieldAccess(E, Field) L level SF SG Sl Msg L ----------------------------------- [L-Error] level SF SG Sl errorExpr(Msg, Ty) L names SG Names Names |{expr}- E ~~> E_P level SF SG Sl E_P L ------------------------ [L-Default]* level SF SG Sl E L ============================= [LA-Nil] levelArgs SF SG Sl nilArgs [] level SF SG Sl E L levelArgs SF SG Sl A Rest ========================================= [LA-Cons] levelArgs SF SG Sl consArgs(E, A) L::Rest =============================================== [LRF-Nil] levelRecFields SF SG Sl nilRecFieldExprs public level SF SG Sl E LE levelRecFields SF SG Sl RF LRF join LE LRF L ===================================================== [LRF-Cons] levelRecFields SF SG Sl consRecFieldExprs(F, E, RF) L /******************************************************************** Statement Security ********************************************************************/ ----------------------- [S-Noop] secure LF SG Sl noop SG secure SF SG Sl S1 SG1 secure SF SG1 Sl S2 SG2 ------------------------------- [S-Seq] secure SF SG Sl seq(S1, S2) SG2 level SF Scope::SG public E public no_lookup Scope X --------------------------------------------- [S-Declare] {secure SF Scope::SG public declare(Ty, X, E) ((X, public)::Scope)::SG} level SF SG Sl E L lookupScopes X SG private ------------------------------- [S-Assign-Private] secure SF SG Sl assign(X, E) SG level SF SG public E public lookupScopes X SG public ----------------------------------- [S-Assign-Public] secure SF SG public assign(X, E) SG level SF SG Sl E L lookupScopes Rec SG private -------------------------------------------- [S-RecUpdate-Private] secure SF SG Sl recUpdate(Rec, Fields, E) SG level SF SG public E public lookupScopes Rec SG public ------------------------------------------------ [S-RecUpdate-Public] secure SF SG public recUpdate(Rec, Fields, E) SG level SF SG Sl E L join L Sl Sl1 secure SF []::SG Sl1 T SGT secure SF []::SG Sl1 F SGF -------------------------------------- [S-IfThenElse] secure SF SG Sl ifThenElse(E, T, F) SG /* We need to split security for while loops into public and private cases because our expressions can set variables. If the condition could set public variables (program counter public) but the level of the condition be private, we could have two evalutaions of the loop, one that immediately uses E-While-False and one that uses E-While-True a few times. This would set the public variable once in the former case but multiple times in the latter, making the values of the public variables differ. Splitting it allows us to ensure we do not set public variables multiple times in one run but not another. */ level SF SG private E L /*safe to have any level here*/ secure SF []::SG private S Scope::SG1 ------------------------------------- [S-While-Private] secure SF SG private while(E, S) SG level SF SG public E public secure SF []::SG public S Scope::SG1 ------------------------------------ [S-While-Public] secure SF SG public while(E, S) SG secure SF []::SG Sl S Scope::SG ------------------------------- [S-ScopeStmt] secure SF SG Sl scopeStmt(S) SG /*only print public values in public situations*/ level SF SG public E public ---------------------------------- [S-Print] secure SF SG public printVal(E) SG level SF Scope::SG Sl E L no_lookup Scope X -------------------------------------------------- [S-Secdecl-Private] {secure SF Scope::SG Sl secdecl(private, Ty, X, E) ((X, private)::Scope)::SG} level SF Scope::SG public E public no_lookup Scope X --------------------------------------- [S-Secdecl-Public] {secure SF Scope::SG public secdecl(public, Ty, X, E) ((X, public)::Scope)::SG} names SG Names Names |{stmt}- S ~~> S_P secure SF SG Sl S_P SG1 ------------------------ [S-Default]* secure SF SG Sl S SG1 /******************************************************************** Function Security ********************************************************************/ /* Note we check function bodies are secure with the program counter starting at the level of the returned variable. This ensures we can set the return variable in the body of the function if it is private. A different approach might be useful for writing programs, but this works for reasoning. */ /*check the function is secure with given info*/ paramSecs Params ParamSecs secure SF [(RetVar, public)::ParamSecs] public Body SG /*check the function ctx agrees with this information*/ lookup SF FunName (public, PSecs) values ParamSecs PSecs ------------------------------------------------------ [FS-Fun] funSecure SF fun(FunName, RetTy, RetVar, RVVal, Params, Body) /*check the function is secure with given info*/ paramSecs Params ParamSecs secure SF [(RetVar, RetLev)::ParamSecs] RetLev Body SG /*check the function ctx agrees with this information*/ lookup SF FunName (RetLev, PSecs) values ParamSecs PSecs ---------------------------------------------------------- [FS-SecFun] funSecure SF secfun(FunName, RetTy, RetLev, RetVar, RVVal, Params, Body) |{fun}- F ~~> F_P funSecure SF F_P ----------------- [FS-Default]* funSecure SF F ================ [FSs-Nil] funsSecure SF [] funSecure SF F funsSecure SF Rest ===================== [FSs-Cons] funsSecure SF F::Rest ------------------------------------ [PS-Param] paramSec param(Name, Ty) Name public ------------------------------------- [PS-SecParam] paramSec secparam(Name, Ty, L) Name L |{param}- P ~~> P_P paramSec P_P Name L ------------------- [PS-Default]* paramSec P Name L =============== [PSs-Nil] paramSecs [] [] paramSec P Name L paramSecs PRest SRest =================================== [PSs-Cons] paramSecs P::PRest (Name, L)::SRest /******************************************************************** Gather Function Information ********************************************************************/ paramSecs Params ParamSecs values ParamSecs PSecs --------------------------------------------- [GFS-Fun] getFunSec fun(Name, RetTy, RetVar, RVVal, Params, Body) Name public PSecs paramSecs Params ParamSecs values ParamSecs PSecs ---------------------------------------------------- [GFS-SecFun] getFunSec secfun(Name, RetTy, RetLev, RetVar, RVVal, Params, Body) Name RetLev PSecs |{fun}- F ~~> F_P getFunSec F_P Name Lev PSecs ---------------------------- [GFS-Default]* getFunSec F Name Lev PSecs ===================== [GFSC-Nil] gatherFunSecCtx [] [] getFunSec F Name Lev PSecs gatherFunSecCtx FRest SRest ==================================================== [GFSC-Cons] gatherFunSecCtx F::FRest (Name, (Lev, PSecs))::SRest /******************************************************************** Program Security ********************************************************************/ gatherFunSecCtx Funs SF getFunSec Main Name RetLev PSecs funsSecure (Name, (RetLev, PSecs))::SF Funs funSecure (Name, (RetLev, PSecs))::SF Main ------------------------------------------- [SP-Program] programSecure program(Funs, Main) PSecs |{program}- P ~~> P_P programSecure P_P PSecs ----------------------- [SP-Default]* programSecure P PSecs
Click on a command or tactic to see a detailed view of its use.
Module exactEval:security. Prove_Constraint exactEval:host:proj_expr_unique. Prove_Constraint exactEval:host:proj_expr_is. Prove_Constraint exactEval:host:proj_expr_other. Prove_Constraint exactEval:host:proj_stmt_unique. [Show Proof] Prove_Constraint exactEval:host:proj_stmt_is. [Show Proof] Prove_Constraint exactEval:host:proj_stmt_other. [Show Proof] Prove_Constraint exactEval:host:proj_fun_unique. [Show Proof] Prove_Constraint exactEval:host:proj_fun_is. [Show Proof] Prove_Constraint exactEval:host:proj_param_unique. [Show Proof] Prove_Constraint exactEval:host:proj_param_is. [Show Proof] Prove_Constraint exactEval:host:proj_program_unique. Prove_Constraint exactEval:host:proj_program_is. Prove_Constraint exactEval:host:proj_typ_unique. Prove_Constraint exactEval:host:proj_typ_is. Extensible_Theorem is_slev_public_or_not : forall L, IsL : is_slev L -> L = public \/ (L = public -> false) on IsL. [Show Proof] Extensible_Theorem is_slev_private_or_not : forall L, IsL : is_slev L -> L = private \/ (L = private -> false) on IsL. [Show Proof] Extensible_Theorem is_slev_eq_or_not : forall L1 L2, IsL1 : is_slev L1 -> IsL2 : is_slev L2 -> L1 = L2 \/ (L1 = L2 -> false) on IsL1. [Show Proof] Add_Proj_Rel exactEval:host:is_expr, exactEval:host:is_args, exactEval:host:is_recFieldExprs, exactEval:host:is_stmt. Prove_Ext_Ind exactEval:host:is_expr, exactEval:host:is_args, exactEval:host:is_recFieldExprs, exactEval:host:is_stmt. [Show Proof] Prove exactEval:host:is_args_nilArgs_or_consArgs. Prove exactEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. Prove exactEval:host:vars_unique. Prove exactEval:host:vars_is. Prove exactEval:host:vars_exist, exactEval:host:varsArgs_exist, exactEval:host:varsRecFields_exist. Prove exactEval:host:stmtNames_is, exactEval:host:stmtNames_isCtx, exactEval:host:exprNames_is. [Show Proof] Prove exactEval:host:stmtNames_unique, exactEval:host:exprNames_unique. [Show Proof] Prove exactEval:host:stmtNames_keep_older. [Show Proof] Prove exactEval:host:stmtNames_exists, exactEval:host:exprNames_exists, exactEval:host:argsNames_exists, exactEval:host:recFieldNames_exists. [Show Proof] Prove exactEval:host:stmtNames_not_in_ctx, exactEval:host:exprNames_not_in_ctx. [Show Proof] Prove exactEval:host:stmtNames_relatedCtxs, exactEval:host:stmtNames_relatedCtxs_ctx_fwd, exactEval:host:stmtNames_relatedCtxs_ctx_back, exactEval:host:exprNames_relatedCtxs. [Show Proof] Prove exactEval:host:stmtNames_increaseCtxs, exactEval:host:stmtNames_increaseCtxs_ctxs, exactEval:host:exprNames_increaseCtxs. [Show Proof] Prove_Constraint exactEval:host:proj_exprNames. Prove_Constraint exactEval:host:proj_stmtNames. [Show Proof] Prove_Constraint exactEval:host:proj_stmtNames_names_forward. [Show Proof] Prove_Constraint exactEval:host:proj_stmtNames_names_backward. [Show Proof] Prove exactEval:host:typeOf_isTy, exactEval:host:stmtOK_isCtx. [Show Proof] Prove exactEval:host:stmtOK_keep_scopes. [Show Proof] Prove exactEval:host:stmtOK_older_scopes_same. [Show Proof] Prove exactEval:host:stmtOK_first_scope_lookup_same. [Show Proof] Prove exactEval:host:typeOf_unique, exactEval:host:stmtOK_unique. [Show Proof] Prove exactEval:host:paramTy_is. [Show Proof] Prove exactEval:host:getFunInfo_is. [Show Proof] Prove exactEval:host:paramTy_exists. [Show Proof] Prove exactEval:host:getFunInfo_exists. [Show Proof] Prove exactEval:host:evalExpr_isCtx, exactEval:host:evalExpr_isValue, exactEval:host:evalStmt_isCtx, exactEval:host:evalArgs_isCtx, exactEval:host:evalArgs_isValue, exactEval:host:evalRecFields_isCtx, exactEval:host:evalRecFields_isValue. [Show Proof] Prove exactEval:host:evalExpr_isOutput, exactEval:host:evalStmt_isOutput, exactEval:host:evalArgs_isOutput, exactEval:host:evalRecFields_isOutput. [Show Proof] Prove exactEval:host:paramName_is. [Show Proof] Prove exactEval:host:getFunEvalInfo_is. [Show Proof] Prove exactEval:host:evalProgram_isOutput. Prove exactEval:host:evalExpr_names_same, exactEval:host:evalStmt_names_same, exactEval:host:evalArgs_names_same, exactEval:host:evalRecFields_names_same. [Show Proof] Prove exactEval:host:evalExpr_newNameScopes, exactEval:host:evalExpr_newNameScopes_output, exactEval:host:evalExpr_newNameScopes_ctx, exactEval:host:evalStmt_newNameScopes_output, exactEval:host:evalStmt_newNameScopes, exactEval:host:evalArgs_newNameScopes, exactEval:host:evalArgs_newNameScopes_output, exactEval:host:evalArgs_newNameScopes_ctx, exactEval:host:evalRecFields_newNameScopes, exactEval:host:evalRecFields_newNameScopes_output, exactEval:host:evalRecFields_newNameScopes_ctx. [Show Proof] Add_Ext_Size exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. Add_Proj_Rel exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. Prove exactEval:host:evalExpr_newNameScopes_exists_ES, exactEval:host:evalStmt_newNameScopes_exists_ES, exactEval:host:evalArgs_newNameScopes_exists_ES, exactEval:host:evalRecFields_newNameScopes_exists_ES. [Show Proof] Prove exactEval:host:evalExpr_ctx_names, exactEval:host:evalStmt_ctx_names, exactEval:host:evalArgs_ctx_names, exactEval:host:evalRecFields_ctx_names. [Show Proof] Prove exactEval:host:evalExpr_newNameScopes_exists_back, exactEval:host:evalStmt_newNameScopes_exists_back, exactEval:host:evalArgs_newNameScopes_exists_back, exactEval:host:evalRecFields_newNameScopes_exists_back. [Show Proof] Prove exactEval:host:evalExpr_scopes_same, exactEval:host:evalExpr_scopes_same_ctx, exactEval:host:evalStmt_scopes_same, exactEval:host:evalStmt_scopes_same_ctx, exactEval:host:evalArgs_scopes_same, exactEval:host:evalArgs_scopes_same_ctx, exactEval:host:evalRecFields_scopes_same, exactEval:host:evalRecFields_scopes_same_ctx. [Show Proof] Prove exactEval:host:evalExpr_scopes_same_exists, exactEval:host:evalStmt_scopes_same_exists, exactEval:host:evalArgs_scopes_same_exists, exactEval:host:evalRecFields_scopes_same_exists. [Show Proof] Prove_Constraint exactEval:host:proj_evalExpr_forward. Prove_Constraint exactEval:host:proj_evalExpr_backward. Prove_Constraint exactEval:host:proj_evalStmt_forward. [Show Proof] Prove_Constraint exactEval:host:proj_evalStmt_backward. [Show Proof] Prove_Ext_Ind exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. [Show Proof] Prove exactEval:host:paramName_unique. [Show Proof] Prove_Constraint exactEval:host:proj_paramName_forward. [Show Proof] Prove_Constraint exactEval:host:proj_paramName_back. [Show Proof] Prove exactEval:host:getFunEvalInfo_unique. [Show Proof] Prove_Constraint exactEval:host:proj_getFunEvalInfo_forward. [Show Proof] Prove_Constraint exactEval:host:proj_getFunEvalInfo_back. [Show Proof] Prove exactEval:host:evalProgram_unique. Prove_Constraint exactEval:host:proj_evalProgram_forward. Prove_Constraint exactEval:host:proj_evalProgram_back. Prove exactEval:host:evalExpr_typePres_ctx, exactEval:host:evalExpr_typePres, exactEval:host:evalStmt_typePres, exactEval:host:evalArgs_typePres_Ctx, exactEval:host:evalArgs_typePres, exactEval:host:evalRecFields_typePres_Ctx, exactEval:host:evalRecFields_typePres. [Show Proof] Prove exactEval:host:paramTy_paramName_same. [Show Proof] Prove exactEval:host:funOK_getFunEvalInfo_related. [Show Proof] Prove exactEval:host:evalExpr_output_forms, exactEval:host:evalStmt_output_forms, exactEval:host:evalArgs_output_forms, exactEval:host:evalRecFields_output_forms. [Show Proof] Prove exactEval:host:evalProgram_output_forms. Prove exactEval:host:paramName_exists. [Show Proof] Prove exactEval:host:getFunEvalInfo_exists. [Show Proof] /******************************************************************** _____ _ _ / ____| (_) | | (___ ___ ___ _ _ _ __ _| |_ _ _ \___ \ / _ \/ __| | | | '__| | __| | | | ____) | __/ (__| |_| | | | | |_| |_| | |_____/ \___|\___|\__,_|_| |_|\__|\__, | __/ | _____ _ |___/ | __ \ | | (_) | |__) | __ ___ _ __ ___ _ __| |_ _ ___ ___ | ___/ '__/ _ \| '_ \ / _ \ '__| __| |/ _ \/ __| | | | | | (_) | |_) | __/ | | |_| | __/\__ \ |_| |_| \___/| .__/ \___|_| \__|_|\___||___/ | | |_| Security Properties ********************************************************************/ /******************************************************************** Properties about join ********************************************************************/ Extensible_Theorem join_is : forall L1 L2 R, Is1 : is_slev L1 -> Is2 : is_slev L2 -> J : join L1 L2 R -> is_slev R on J. [Show Proof] %need this because we can't analyze it due to restrictions Extensible_Theorem join_private_right : forall L R, Is : is_slev L -> J : join L private R -> R = private on J. [Show Proof] Extensible_Theorem join_unique : forall L1 L2 LA LB, Is1 : is_slev L1 -> Is2 : is_slev L2 -> JA : join L1 L2 LA -> JB : join L1 L2 LB -> LA = LB on JA. [Show Proof] Extensible_Theorem join_private : forall L1 L2, Is1 : is_slev L1 -> Is2 : is_slev L2 -> J : join L1 L2 private -> L1 = private \/ L2 = private on J. [Show Proof] Extensible_Theorem join_public : forall L1 L2, Is1 : is_slev L1 -> Is2 : is_slev L2 -> J : join L1 L2 public -> L1 = public /\ L2 = public on J. [Show Proof] /******************************************************************** Security is ********************************************************************/ Theorem lookup_is_slev : forall L X Lev, is_list (is_pair is_string is_slev) L -> lookup L X Lev -> is_slev Lev. [Show Proof] Theorem lookupScopes_is_slev : forall SG X Lev, is_list (is_list (is_pair is_string is_slev)) SG -> lookupScopes X SG Lev -> is_slev Lev. [Show Proof] Theorem lookupSecFun_is : forall SF F Lev PLs, is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> lookup SF F (Lev, PLs) -> is_slev Lev /\ is_list is_slev PLs. [Show Proof] Theorem domain_is_sec : forall L D, is_list (is_pair is_string is_slev) L -> domain L D -> is_list is_string D. [Show Proof] Theorem names_is_sec : forall SG Names, is_list (is_list (is_pair is_string is_slev)) SG -> names SG Names -> is_list is_string Names. [Show Proof] Theorem mem_is_sec : forall L IDS, is_list (is_pair is_string is_slev) L -> mem IDS L -> is_pair is_string is_slev IDS. [Show Proof] Extensible_Theorem level_is : forall SF SG PC E L, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> Lev : level SF SG PC E L -> is_slev L on Lev as IH_E, secure_is : forall SF SG PC S SG', IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> Sec : secure SF SG PC S SG' -> is_list (is_list (is_pair is_string is_slev)) SG' on Sec as IH_S also levelArgs_is : forall SF SG PC A L, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> Lev : levelArgs SF SG PC A L -> is_list is_slev L on Lev as IH_A, levelRecFields_is : forall SF SG PC RF L, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> Lev : levelRecFields SF SG PC RF L -> is_slev L on Lev as IH_RF. [Show Proof] /******************************************************************** Uniqueness of security ********************************************************************/ Extensible_Theorem level_unique : forall SF SG PC E LA LB, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> LevA : level SF SG PC E LA -> LevB : level SF SG PC E LB -> LA = LB on LevA as IH_E, secure_unique : forall SF SG PC S SGA SGB, IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> SecA : secure SF SG PC S SGA -> SecB : secure SF SG PC S SGB -> SGA = SGB on SecA as IH_S also levelArgs_unique : forall SF SG PC A LA LB, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> LevA : levelArgs SF SG PC A LA -> LevB : levelArgs SF SG PC A LB -> LA = LB on LevA as IH_A, levelRecFields_unique : forall SF SG PC RF LA LB, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> LevA : levelRecFields SF SG PC RF LA -> LevB : levelRecFields SF SG PC RF LB -> LA = LB on LevA as IH_RF. [Show Proof] /******************************************************************** Uniqueness of security ********************************************************************/ Extensible_Theorem secure_older_scopes : forall SF Scope SG PC S SG', IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) (Scope::SG) -> Sec : secure SF (Scope::SG) PC S SG' -> exists Scope', SG' = Scope'::SG /\ (forall X L, lookup Scope X L -> lookup Scope' X L) on Sec. [Show Proof] /******************************************************************** Names in contexts related ********************************************************************/ Theorem names_same_scopes_same[V] : forall A B (C : list (list (pair string V))), is_list (is_list (is_pair is_string is_value)) A -> is_list (is_list (is_pair is_string is_value)) B -> names_same A C -> scopes_same A B -> names_same B C. [Show Proof] Theorem zip_names_same[A, B] : forall (Names : list string) (A : list A) (B : list B) ZA ZB, zip Names A ZA -> zip Names B ZB -> names_same [ZA] [ZB]. [Show Proof] Extensible_Theorem level_eval_names_same : forall E SF SG PC L FE EE V EE' O, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> NS : names_same EE SG -> Ev : evalExpr FE EE E V EE' O -> Lev : level SF SG PC E L -> names_same EE' SG on Ev, secure_eval_names_same : forall S SF SG PC SG' FE Scope EE EE' O, IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> NS : names_same (Scope::EE) SG -> Ev : evalStmt FE (Scope::EE) S EE' O -> Sec : secure SF SG PC S SG' -> names_same EE' SG' on Ev, levelArgs_eval_names_same : forall A SF SG PC L FE EE V EE' O, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> NS : names_same EE SG -> Ev : evalArgs FE EE A V EE' O -> Lev : levelArgs SF SG PC A L -> names_same EE' SG on Ev, levelRecFields_eval_names_same : forall RF SF SG PC L FE EE V EE' O, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> NS : names_same EE SG -> Ev : evalRecFields FE EE RF V EE' O -> Lev : levelRecFields SF SG PC RF L -> names_same EE' SG on Ev. [Show Proof] /******************************************************************** Properties of public_equiv ********************************************************************/ Define public_equiv : list (list (pair string slev)) -> list (list (pair string value)) -> list (list (pair string value)) -> prop by public_equiv [] [] []; public_equiv (SScope::S) (Scope1::G1) (Scope2::G2) := %lookup same for public (forall X V, lookup SScope X public -> lookup Scope1 X V -> lookup Scope2 X V) /\ (forall X V, lookup SScope X public -> lookup Scope2 X V -> lookup Scope1 X V) /\ %rest public_equiv S G1 G2. Theorem no_lookup_names_same : forall A B X, is_list (is_pair is_string is_value) B -> (forall X IB, mem (X, IB) B -> exists (IA : value), mem (X, IA) A) -> no_lookup A X -> no_lookup B X. [Show Proof] Theorem public_equiv_lookupScopes : forall S G1 G2 X V, public_equiv S G1 G2 -> names_same G1 S -> names_same G2 S -> is_list (is_list (is_pair is_string is_value)) G2 -> lookupScopes X S public -> lookupScopes X G1 V -> lookupScopes X G2 V. [Show Proof] 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_refl : forall SG G, names_same G SG -> public_equiv SG G G. [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_scopes_same_snd : forall SG G GA GB, public_equiv SG G GB -> scopes_same GA GB -> public_equiv SG G GA. [Show Proof] Theorem public_equiv_scopes_same_fst : forall SG G GA GB, public_equiv SG GB G -> scopes_same GA GB -> public_equiv SG GA G. [Show Proof] Theorem public_equiv_add_scope : forall SG GA GB, public_equiv SG GA GB -> public_equiv ([]::SG) ([]::GA) ([]::GB). [Show Proof] Theorem public_equiv_add_public : forall SS SG AS GA BS GB X V, public_equiv (SS::SG) (AS::GA) (BS::GB) -> public_equiv (((X, public)::SS)::SG) (((X, V)::AS)::GA) (((X, V)::BS)::GB). [Show Proof] Theorem public_equiv_add_other : forall SS SG AS GA BS GB X L VA VB, public_equiv (SS::SG) (AS::GA) (BS::GB) -> (L = public -> false) -> public_equiv (((X, L)::SS)::SG) (((X, VA)::AS)::GA) (((X, VB)::BS)::GB). [Show Proof] Theorem remove_all_eq_or_mem[Key, Item] : forall L L' (X Y : Key) (V : Item), remove_all L X L' -> mem (Y, V) L -> Y = X \/ mem (Y, V) L'. [Show Proof] Theorem public_equiv_replaceScopes_public : forall SG GA GB X V RA RB, public_equiv SG GA GB -> names_same GA SG -> names_same GB SG -> lookupScopes X SG public -> replaceScopes X V GA RA -> replaceScopes X V GB RB -> public_equiv SG RA RB. [Show Proof] Theorem public_equiv_replaceScopes_other : forall SG GA GB X L VA VB RA RB, public_equiv SG GA GB -> names_same GA SG -> names_same GB SG -> lookupScopes X SG L -> (L = public -> false) -> replaceScopes X VA GA RA -> replaceScopes X VB GB RB -> public_equiv SG RA RB. [Show Proof] Theorem replaceScopes_public_equiv : forall SG L X V L' SL, names_same L SG -> replaceScopes X V L L' -> lookupScopes X SG SL -> (SL = public -> false) -> public_equiv SG L L'. [Show Proof] /******************************************************************** No public changes in private contexts ********************************************************************/ Extensible_Theorem stmt_not_public_no_public_change : forall S SF SScope SG PC SG' FE Scope EE Scope' EE' O, IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) (SScope::SG) -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> NS : names_same (Scope::EE) (SScope::SG) -> Ev : evalStmt FE (Scope::EE) S (Scope'::EE') O -> Sec : secure SF (SScope::SG) PC S SG' -> NEq : (PC = public -> false) -> /*only the end of the ctxs are related, not the first scope*/ public_equiv SG EE EE' on Ev as IH_S, expr_not_public_no_public_change : forall E SF SG PC L FE EE V EE' O, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> NS : names_same EE SG -> Ev : evalExpr FE EE E V EE' O -> Lev : level SF SG PC E L -> NEq : (PC = public -> false) -> public_equiv SG EE EE' on Ev as IH_E, args_not_public_no_public_change : forall A SF SG PC L FE EE V EE' O, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> NS : names_same EE SG -> Ev : evalArgs FE EE A V EE' O -> Lev : levelArgs SF SG PC A L -> NEq : (PC = public -> false) -> public_equiv SG EE EE' on Ev as IH_A, recFields_not_public_no_public_change : forall RF SF SG PC L FE EE V EE' O, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> NS : names_same EE SG -> Ev : evalRecFields FE EE RF V EE' O -> Lev : levelRecFields SF SG PC RF L -> NEq : (PC = public -> false) -> public_equiv SG EE EE' on Ev as IH_RF. [Show Proof] Theorem while_no_public_change : forall SF SG PC SG' L Cond Body FE EE EE2 O, is_expr Cond -> is_stmt Body -> is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> is_list (is_list (is_pair is_string is_slev)) SG -> is_slev PC -> is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> is_list (is_list (is_pair is_string is_value)) EE -> names_same EE SG -> secure SF SG PC (while Cond Body) SG' -> level SF SG PC Cond L -> (L = public -> false) -> evalStmt FE EE (while Cond Body) EE2 O -> public_equiv SG EE EE2. [Show Proof] /******************************************************************** Evaluation does not leak private information ********************************************************************/ %all public argument values are the same; private ones may differ Define level_arg_vals : list slev -> list value -> list value -> prop by level_arg_vals [] [] []; level_arg_vals (public::SRest) (V::ARest) (V::BRest) := level_arg_vals SRest ARest BRest; level_arg_vals (L::SRest) (VA::ARest) (VB::BRest) := (L = public -> false) /\ level_arg_vals SRest ARest BRest. Theorem zip_level_arg_vals : forall S A B N ZA ZB ZS, level_arg_vals S A B -> zip N A ZA -> zip N B ZB -> zip N S ZS -> public_equiv [ZS] [ZA] [ZB]. [Show Proof] Theorem zip_is_sec : forall A B Z, is_list is_string A -> is_list is_slev B -> zip A B Z -> is_list (is_pair is_string is_slev) Z. [Show Proof] %security and evaluation fun ctxs are appropriately related Define secFunCtxs : list (pair string (pair slev (list slev))) -> list (pair string (pair string (pair value (pair (list string) stmt)))) -> prop by secFunCtxs SF FE := forall FName RetLev PSecs RetVar RVVal PNames Body, lookup SF FName (RetLev, PSecs) -> lookup FE FName (RetVar, RVVal, PNames, Body) -> exists ZP SG, zip PNames PSecs ZP /\ secure SF [(RetVar, RetLev)::ZP] RetLev Body SG. Extensible_Theorem %evaluation under public_equiv ctxs yields public_equiv ctxs stmt_secure : forall S SF SG PC SG' FE ScopeA EE_A EE_A' OA ScopeB EE_B EE_B' OB, IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) (ScopeA::EE_A) -> IsEE_B : is_list (is_list (is_pair is_string is_value)) (ScopeB::EE_B) -> SFC : secFunCtxs SF FE -> NSA : names_same (ScopeA::EE_A) SG -> NSB : names_same (ScopeB::EE_B) SG -> PE : public_equiv SG (ScopeA::EE_A) (ScopeB::EE_B) -> Sec : secure SF SG PC S SG' -> EvA : evalStmt FE (ScopeA::EE_A) S EE_A' OA -> EvB : evalStmt FE (ScopeB::EE_B) S EE_B' OB -> public_equiv SG' EE_A' EE_B' on EvA as IH_S, expr_secure : forall E SF SG PC L FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : level SF SG PC E L -> EvA : evalExpr FE EE_A E VA EE_A' OA -> EvB : evalExpr FE EE_B E VB EE_B' OB -> public_equiv SG EE_A' EE_B' on EvA as IH_E, args_secure : forall A SF SG PC L FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : levelArgs SF SG PC A L -> EvA : evalArgs FE EE_A A VA EE_A' OA -> EvB : evalArgs FE EE_B A VB EE_B' OB -> public_equiv SG EE_A' EE_B' on EvA as IH_A, recFields_secure : forall RF SF SG PC L FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : levelRecFields SF SG PC RF L -> EvA : evalRecFields FE EE_A RF VA EE_A' OA -> EvB : evalRecFields FE EE_B RF VB EE_B' OB -> public_equiv SG EE_A' EE_B' on EvA as IH_RF, %public terms produce the same values under public_equiv ctxs expr_level : forall E SF SG PC FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : level SF SG PC E public -> EvA : evalExpr FE EE_A E VA EE_A' OA -> EvB : evalExpr FE EE_B E VB EE_B' OB -> VA = VB on EvA as IH_E_L, recFields_level : forall RF SF SG PC FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : levelRecFields SF SG PC RF public -> EvA : evalRecFields FE EE_A RF VA EE_A' OA -> EvB : evalRecFields FE EE_B RF VB EE_B' OB -> VA = VB on EvA as IH_RF_L, %arguments produce the same values for public ones args_level : forall A SF SG PC Ls FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : levelArgs SF SG PC A Ls -> EvA : evalArgs FE EE_A A VA EE_A' OA -> EvB : evalArgs FE EE_B A VB EE_B' OB -> level_arg_vals Ls VA VB on EvA as IH_A_L. [Show Proof] Extensible_Theorem stmt_not_public_no_output : forall S SF SG PC SG' FE Scope EE EE' O, IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) (Scope::EE) -> SFC : secFunCtxs SF FE -> NS : names_same (Scope::EE) SG -> Ev : evalStmt FE (Scope::EE) S EE' O -> Sec : secure SF SG PC S SG' -> NEq : (PC = public -> false) -> O = [] on Ev as IH_S, expr_not_public_no_output : forall E SF SG PC L FE EE V EE' O, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> SFC : secFunCtxs SF FE -> NS : names_same EE SG -> Ev : evalExpr FE EE E V EE' O -> Lev : level SF SG PC E L -> NEq : (PC = public -> false) -> O = [] on Ev as IH_E, args_not_public_no_output : forall A SF SG PC L FE EE V EE' O, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> SFC : secFunCtxs SF FE -> NS : names_same EE SG -> Ev : evalArgs FE EE A V EE' O -> Lev : levelArgs SF SG PC A L -> NEq : (PC = public -> false) -> O = [] on Ev as IH_A, recFields_not_public_no_output : forall RF SF SG PC L FE EE V EE' O, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE : is_list (is_list (is_pair is_string is_value)) EE -> SFC : secFunCtxs SF FE -> NS : names_same EE SG -> Ev : evalRecFields FE EE RF V EE' O -> Lev : levelRecFields SF SG PC RF L -> NEq : (PC = public -> false) -> O = [] on Ev as IH_RF. [Show Proof] Extensible_Theorem secure_output : forall S SF SG PC SG' FE ScopeA EE_A EE_A' OA ScopeB EE_B EE_B' OB, IsS : is_stmt S -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) (ScopeA::EE_A) -> IsEE_B : is_list (is_list (is_pair is_string is_value)) (ScopeB::EE_B) -> SFC : secFunCtxs SF FE -> NSA : names_same (ScopeA::EE_A) SG -> NSB : names_same (ScopeB::EE_B) SG -> PE : public_equiv SG (ScopeA::EE_A) (ScopeB::EE_B) -> Sec : secure SF SG PC S SG' -> EvA : evalStmt FE (ScopeA::EE_A) S EE_A' OA -> EvB : evalStmt FE (ScopeB::EE_B) S EE_B' OB -> OA = OB on EvA as IH_S, expr_secure_output : forall E SF SG PC L FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsE : is_expr E -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : level SF SG PC E L -> EvA : evalExpr FE EE_A E VA EE_A' OA -> EvB : evalExpr FE EE_B E VB EE_B' OB -> OA = OB on EvA as IH_E, args_secure_output : forall A SF SG PC L FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsA : is_args A -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : levelArgs SF SG PC A L -> EvA : evalArgs FE EE_A A VA EE_A' OA -> EvB : evalArgs FE EE_B A VB EE_B' OB -> OA = OB on EvA as IH_A, recFields_secure_output : forall RF SF SG PC L FE EE_A EE_A' VA OA EE_B EE_B' VB OB, IsRF : is_recFieldExprs RF -> IsSF : is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF -> IsSG : is_list (is_list (is_pair is_string is_slev)) SG -> IsPC : is_slev PC -> IsFE : is_list (is_pair is_string (is_pair is_string (is_pair is_value (is_pair (is_list is_string) is_stmt)))) FE -> IsEE_A : is_list (is_list (is_pair is_string is_value)) EE_A -> IsEE_B : is_list (is_list (is_pair is_string is_value)) EE_B -> SFC : secFunCtxs SF FE -> NSA : names_same EE_A SG -> NSB : names_same EE_B SG -> PE : public_equiv SG EE_A EE_B -> Lev : levelRecFields SF SG PC RF L -> EvA : evalRecFields FE EE_A RF VA EE_A' OA -> EvB : evalRecFields FE EE_B RF VB EE_B' OB -> OA = OB on EvA as IH_RF. [Show Proof] /******************************************************************** Programs do not leak private information ********************************************************************/ %-------------------------------------------- % Everything gathered has is relations %-------------------------------------------- Extensible_Theorem paramSec_is : forall P Name L, IsP : is_param P -> PS : paramSec P Name L -> is_string Name /\ is_slev L on PS. [Show Proof] Theorem paramSecs_is : forall Ps PSecs, is_list is_param Ps -> paramSecs Ps PSecs -> is_list (is_pair is_string is_slev) PSecs. [Show Proof] Theorem values_is_sec : forall L V, is_list (is_pair is_string is_slev) L -> values L V -> is_list is_slev V. [Show Proof] Extensible_Theorem getFunSec_is : forall F Name RetLev PSecs, IsF : is_fun F -> GFS : getFunSec F Name RetLev PSecs -> is_string Name /\ is_slev RetLev /\ is_list is_slev PSecs on GFS. [Show Proof] Theorem gatherFunSecCtx_is : forall Fs SF, is_list is_fun Fs -> gatherFunSecCtx Fs SF -> is_list (is_pair is_string (is_pair is_slev (is_list is_slev))) SF. [Show Proof] Extensible_Theorem program_secure_is : forall P S, IsP : is_program P -> Sec : programSecure P S -> is_list is_slev S on Sec. [Show Proof] %-------------------------------------------- % Everything gathered is unique %-------------------------------------------- Extensible_Theorem paramSec_unique : forall P NameA LA NameB LB, IsP : is_param P -> PSA : paramSec P NameA LA -> PSB : paramSec P NameB LB -> NameA = NameB /\ LA = LB on PSA. [Show Proof] Theorem paramSecs_unique : forall Ps PSecsA PSecsB, is_list is_param Ps -> paramSecs Ps PSecsA -> paramSecs Ps PSecsB -> PSecsA = PSecsB. [Show Proof] Extensible_Theorem getFunSec_unique : forall F NA LA PSA NB LB PSB, IsF : is_fun F -> GFSA : getFunSec F NA LA PSA -> GFSB : getFunSec F NB LB PSB -> NA = NB /\ LA = LB /\ PSA = PSB on GFSA. [Show Proof] Theorem gatherFunSecCtx_unique : forall Fs SFA SFB, is_list is_fun Fs -> gatherFunSecCtx Fs SFA -> gatherFunSecCtx Fs SFB -> SFA = SFB. [Show Proof] Extensible_Theorem program_secure_unique : forall P A B, IsP : is_program P -> SecA : programSecure P A -> SecB : programSecure P B -> A = B on SecA. [Show Proof] %-------------------------------------------- % Gathered security and eval info are related %-------------------------------------------- Extensible_Theorem paramName_paramSec : forall P N NS L, IsP : is_param P -> PN : paramName P N -> PS : paramSec P NS L -> N = NS on PS. [Show Proof] Theorem paramNames_paramSecs : forall Ps PNs PSecs, is_list is_param Ps -> paramNames Ps PNs -> paramSecs Ps PSecs -> domain PSecs PNs. [Show Proof] Theorem domain_values_zip[A, B] : forall (L : list (pair A B)) D V, domain L D -> values L V -> zip D V L. [Show Proof] Extensible_Theorem getFun_sec : forall F FName RetVar RVVal PNames Body SName RetLev PSecs SF, IsF : is_fun F -> GFEI : getFunEvalInfo F FName RetVar RVVal PNames Body -> GFS : getFunSec F SName RetLev PSecs -> FS : funSecure SF F -> exists ZP SG, FName = SName /\ zip PNames PSecs ZP /\ secure SF [(RetVar, RetLev)::ZP] RetLev Body SG on GFS. [Show Proof] %can't do secFunCtxs directly due to need to use SF_Full, % but this lets us build it Theorem gatherCtxs_secFunCtxs : forall Fs SF FE SF_Full FName RetLev PSecs RetVar RVVal PNames Body, is_list is_fun Fs -> gatherFunSecCtx Fs SF -> getFunEvalCtx Fs FE -> funsSecure SF_Full Fs -> lookup SF FName (RetLev, PSecs) -> lookup FE FName (RetVar, RVVal, PNames, Body) -> exists ZP SG, zip PNames PSecs ZP /\ secure SF_Full [(RetVar, RetLev)::ZP] RetLev Body SG. [Show Proof] %-------------------------------------------- % Secure programs do not leak in output %-------------------------------------------- Extensible_Theorem program_secure : forall P A_S A_A A_B O_A O_B, IsP : is_program P -> IsA_A : is_list is_value A_A -> IsA_B : is_list is_value A_B -> Sec : programSecure P A_S -> %different sets of arguments to main have the same public args, % but may differ in private args Rel : level_arg_vals A_S A_A A_B -> EvA : evalProgram A_A P O_A -> EvB : evalProgram A_B P O_B -> O_A = O_B on Sec. [Show Proof] /* We frame program security as having the same output if the public arguments to main are the same. The concept of non-public arguments to main sounds a bit strange; isn't the user, the person from whom we are hiding private information, giving all the arguments? We can think of private arguments as standing in for the contents of files and such, so a private argument might be an encryption key for the program read from the file. Therefore it does make sense to have non-public arguments to main. */ /* The security extension as written isn't very useful. Suppose we want to write a password checker, a good use for information flow security, using it. We take the true password and a user's attempt as arguments to main, compare them, and find we cannot output whether they matched because the true password is private, and thus the result of comparing them is also private and cannot be printed. A "real" version of this extension, intended to be used for writing real programs, would need a declassify construct to lower information to a public level. Such a construct is unsound for security, which is why we don't include it here where we are concerned with proving soundness, not writing actual programs. However, it allows a programmer to decide explicitly what private information may escape and in what circumstances, so it is effectively good enough. For example, telling the user the passwords matched or didn't leaks a little bit of information to the user about the true password, but the programmer decides this is still secure enough and necessary for the job the program is doing. */