From 872eb6b59a7018e45686f6ed77c9f730a251963c Mon Sep 17 00:00:00 2001 From: akashlal Date: Sun, 5 Apr 2015 19:45:38 +0530 Subject: VC gen for security properties --- Source/Core/CommandLineOptions.cs | 6 +- Source/ExecutionEngine/ExecutionEngine.cs | 9 +- Source/Provers/SMTLib/ProverInterface.cs | 3 +- Source/VCGeneration/StratifiedVC.cs | 381 +++++++++++++++++++++++++++++- 4 files changed, 392 insertions(+), 7 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index bbdccda9..dbbb6fd0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -746,6 +746,7 @@ namespace Microsoft.Boogie { public bool PrintInlined = false; public bool ExtractLoops = false; public bool DeterministicExtractLoops = false; + public string SecureVcGen = null; public int StratifiedInlining = 0; public string FixedPointEngine = null; public int StratifiedInliningOption = 0; @@ -1251,7 +1252,10 @@ namespace Microsoft.Boogie { } } return true; - + case "secure": + if (ps.ConfirmArgumentCount(1)) + SecureVcGen = args[ps.i]; + return true; case "stratifiedInline": if (ps.ConfirmArgumentCount(1)) { switch (args[ps.i]) { diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 7756973d..31a69c6e 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1060,6 +1060,9 @@ namespace Microsoft.Boogie #endregion + if (SecureVCGen.outfile != null) + SecureVCGen.outfile.Close(); + return outcome; } @@ -1290,9 +1293,13 @@ namespace Microsoft.Boogie { vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers); } + else if (CommandLineOptions.Clo.SecureVcGen != null) + { + vcgen = new SecureVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers); + } else { - vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers); + vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers); } return vcgen; } diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index a62fa25a..868b9ee3 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -74,7 +74,8 @@ namespace Microsoft.Boogie.SMTLib SetupProcess(); - if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer) + if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer + || CommandLineOptions.Clo.SecureVcGen != null) { // Prepare for ApiChecker usage if (options.LogFilename != null && currentLogFile == null) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 88577e46..6f8d3668 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2094,10 +2094,7 @@ namespace VC { } // end FCallInliner - public class EmptyErrorHandler : ProverInterface.ErrorHandler { - public override void OnModel(IList labels, Model model, ProverInterface.Outcome proverOutcome) - { } - } + public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler { Dictionary implName2StratifiedInliningInfo; @@ -2538,4 +2535,380 @@ namespace VC { } // class StratifiedVCGen + public class EmptyErrorHandler : ProverInterface.ErrorHandler + { + public override void OnModel(IList labels, Model model, ProverInterface.Outcome proverOutcome) + { } + } + + public class InvalidProgramForSecureVc : Exception + { + public InvalidProgramForSecureVc(string msg) : + base(msg) { } + } + + public class SecureVCGen : VCGen + { + // Z3 + ProverInterface prover; + // Handler + ErrorReporter handler; + // dump file + public static TokenTextWriter outfile = null; + + + public SecureVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List checkers) + : base(program, logFilePath, appendLogFile, checkers) + { + prover = null; + handler = null; + if (CommandLineOptions.Clo.SecureVcGen != "" && outfile == null) + { + outfile = new TokenTextWriter(new StreamWriter(CommandLineOptions.Clo.SecureVcGen)); + CommandLineOptions.Clo.PrintInstrumented = true; + var implsToVerify = new HashSet( + program.TopLevelDeclarations.OfType() + .Where(impl => !impl.SkipVerification) + .Select(impl => impl.Name)); + + foreach (var decl in program.TopLevelDeclarations) + { + if (decl is NamedDeclaration && implsToVerify.Contains((decl as NamedDeclaration).Name)) + continue; + decl.Emit(outfile, 0); + } + } + } + + private Block GetExitBlock(Implementation impl) + { + var exitblocks = impl.Blocks.Where(blk => blk.TransferCmd is ReturnCmd); + if (exitblocks.Count() == 1) + return exitblocks.First(); + // create a new exit block + var eb = new Block(Token.NoToken, "SVCeb", new List(), new ReturnCmd(Token.NoToken)); + foreach (var b in exitblocks) + { + b.TransferCmd = new GotoCmd(Token.NoToken, new List { eb }); + } + impl.Blocks.Add(eb); + return eb; + } + + //static int LocalVarCounter = 0; + private LocalVariable GetNewLocal(Variable v, string suffix) + { + return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, + string.Format("svc_{0}_{1}", v.Name, suffix), v.TypedIdent.Type)); + } + + private void GenVc(Implementation impl, VerifierCallback collector) + { + if (impl.Proc.Requires.Any()) + throw new InvalidProgramForSecureVc("SecureVc: Requires not supported"); + if(impl.LocVars.Any(v => isVisible(v))) + throw new InvalidProgramForSecureVc("SecureVc: Visible Local variables not allowed"); + + // Gather spec, remove existing ensures + var secureAsserts = new List(); + var logicalAsserts = new List(); + + foreach (var ens in impl.Proc.Ensures) + { + if(ens.Free) + throw new InvalidProgramForSecureVc("SecureVc: Free Ensures not supported"); + var dd = new Duplicator(); + secureAsserts.Add(new AssertCmd(ens.tok, Expr.Not(ens.Condition))); + logicalAsserts.Add(dd.VisitAssertCmd(new AssertCmd(ens.tok, ens.Condition)) as AssertCmd); + } + impl.Proc.Ensures.Clear(); + + // Make a copy of the impl + var dup = new Duplicator(); + var implDup = dup.VisitImplementation(impl); + + // Get exit block + var eb = GetExitBlock(impl); + + // Create two blocks: one for secureAsserts, one for logical asserts + var ebSecure = new Block(Token.NoToken, "svc_secure_asserts", new List(), new ReturnCmd(Token.NoToken)); + var ebLogical = new Block(Token.NoToken, "svc_logical_asserts", new List(), new ReturnCmd(Token.NoToken)); + + eb.TransferCmd = new GotoCmd(eb.TransferCmd.tok, new List { ebSecure, ebLogical }); + impl.Blocks.Add(ebSecure); + impl.Blocks.Add(ebLogical); + + // Rename spec, while create copies of the hidden variables + var substOld = new Dictionary(); + var substVarSpec = new Dictionary(); + var substVarPath = new Dictionary(); + foreach (var g in program.GlobalVariables) + { + if (!isHidden(g)) continue; + var lv = GetNewLocal(g, "In"); + impl.LocVars.Add(lv); + substOld.Add(g, Expr.Ident(lv)); + } + + for(int i = 0; i < impl.InParams.Count; i++) + { + var v = impl.Proc.InParams[i]; + if (!isHidden(v)) + { + substVarSpec.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i])); + continue; + } + + var lv = GetNewLocal(v, "In"); + impl.LocVars.Add(lv); + substVarSpec.Add(v, Expr.Ident(lv)); + substVarPath.Add(impl.InParams[i], Expr.Ident(lv)); + } + + for (int i = 0; i < impl.OutParams.Count; i++) + { + var v = impl.Proc.OutParams[i]; + if (!isHidden(v)) + { + substVarSpec.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i])); + continue; + } + + var lv = GetNewLocal(v, "Out"); + impl.LocVars.Add(lv); + substVarSpec.Add(v, Expr.Ident(lv)); + substVarPath.Add(impl.OutParams[i], Expr.Ident(lv)); + } + + foreach (var g in program.GlobalVariables) + { + if (!isHidden(g)) continue; + if (!impl.Proc.Modifies.Any(ie => ie.Name == g.Name)) continue; + + var lv = GetNewLocal(g, "Out"); + impl.LocVars.Add(lv); + substVarSpec.Add(g, Expr.Ident(lv)); + substVarPath.Add(g, Expr.Ident(lv)); + } + + secureAsserts = secureAsserts.ConvertAll(ac => + Substituter.ApplyReplacingOldExprs( + Substituter.SubstitutionFromHashtable(substVarSpec), + Substituter.SubstitutionFromHashtable(substOld), + ac) as AssertCmd); + + var substVarProcToImpl = new Dictionary(); + for (int i = 0; i < impl.InParams.Count; i++) + substVarProcToImpl.Add(impl.Proc.InParams[i], Expr.Ident(impl.InParams[i])); + + for (int i = 0; i < impl.OutParams.Count; i++) + substVarProcToImpl.Add(impl.Proc.OutParams[i], Expr.Ident(impl.OutParams[i])); + + logicalAsserts = logicalAsserts.ConvertAll(ac => + Substituter.Apply(Substituter.SubstitutionFromHashtable(substVarProcToImpl), ac) + as AssertCmd); + + // Paths + foreach (var path in GetAllPaths(implDup)) + { + var wp = ComputeWP(implDup, path); + + // replace hidden variables to match those used in the spec + wp = Substituter.ApplyReplacingOldExprs( + Substituter.SubstitutionFromHashtable(substVarPath), + Substituter.SubstitutionFromHashtable(substOld), + wp); + + ebSecure.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(wp))); + } + + ebSecure.Cmds.AddRange(secureAsserts); + ebLogical.Cmds.AddRange(logicalAsserts); + + if (outfile != null) + { + impl.Proc.Emit(outfile, 0); + impl.Emit(outfile, 0); + } + + ModelViewInfo mvInfo; + ConvertCFG2DAG(impl); + var gotoCmdOrigins = PassifyImpl(impl, out mvInfo); + + var gen = prover.VCExprGen; + var exprGen = prover.Context.ExprGen; + var translator = prover.Context.BoogieExprTranslator; + + var label2absy = new Dictionary(); + VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, prover.Context); + translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); + var implVc = gen.Not(GenerateVCAux(impl, null, label2absy, prover.Context)); + + handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, prover.Context, program); + + prover.Assert(implVc, true); + } + + Expr ComputeWP(Implementation impl, List path) + { + Expr expr = Expr.True; + + // create constants for out varibles + var subst = new Dictionary(); + foreach (var g in impl.Proc.Modifies) + { + var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, + "svc_out_const_" + g.Name, g.Decl.TypedIdent.Type)); + subst.Add(c, g); + expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), g)); + } + + foreach (var v in impl.OutParams) + { + var c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, + "svc_out_const_" + v.Name, v.TypedIdent.Type)); + subst.Add(c, Expr.Ident(v)); + expr = Expr.And(expr, Expr.Eq(Expr.Ident(c), Expr.Ident(v))); + } + + // we need this technicality + var subst1 = new Dictionary(); + foreach (var g in program.GlobalVariables) + { + subst1.Add(g, new OldExpr(Token.NoToken, Expr.Ident(g))); + } + + // Implicitly close with havoc of all the locals and OutParams + path.Insert(0, new HavocCmd(Token.NoToken, new List( + impl.LocVars.Select(v => Expr.Ident(v)).Concat( + impl.OutParams.Select(v => Expr.Ident(v)))))); + + for (int i = path.Count - 1; i >= 0; i--) + { + var cmd = path[i]; + if (cmd is AssumeCmd) + { + expr = Expr.And(expr, (cmd as AssumeCmd).Expr); + } + else if (cmd is AssignCmd) + { + var h = new Dictionary(); + var acmd = cmd as AssignCmd; + for (int j = 0; j < acmd.Lhss.Count; j++) + { + h.Add(acmd.Lhss[j].DeepAssignedVariable, acmd.Rhss[j]); + } + var s = Substituter.SubstitutionFromHashtable(h); + expr = Substituter.Apply(s, expr); + } + else if (cmd is HavocCmd) + { + var h = new Dictionary(); + var formals = new List(); + + var vc = new VariableCollector(); + vc.VisitExpr(expr); + + foreach (var ie in (cmd as HavocCmd).Vars) + { + if (!vc.usedVars.Contains(ie.Decl)) continue; + var f = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, + ie.Decl.Name + "_formal", ie.Decl.TypedIdent.Type)); + h.Add(ie.Decl, Expr.Ident(f)); + formals.Add(f); + } + if (!formals.Any()) + continue; + var s = Substituter.SubstitutionFromHashtable(h); + expr = Substituter.Apply(s, expr); + expr = new ExistsExpr(Token.NoToken, formals, expr); + } + else + { + throw new InvalidProgramForSecureVc(string.Format("Unhandled cmd: {0}", cmd)); + } + } + + // Implicitly close with havoc of all the locals and OutParams + + + + expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst1), expr); + expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), + Substituter.SubstitutionFromHashtable(new Dictionary()), expr); + expr.Typecheck(new TypecheckingContext(null)); + return expr; + } + + // Generate all paths in the impl + IEnumerable> GetAllPaths(Implementation impl) + { + var stk = new Stack>(); + stk.Push(Tuple.Create(impl.Blocks[0], 0)); + + while (stk.Any()) + { + var tup = stk.Peek(); + if (tup.Item1.TransferCmd is ReturnCmd) + { + var ret = new List(); + var ls = stk.ToList(); + ls.Iter(t => ret.AddRange(t.Item1.Cmds)); + yield return ret; + + stk.Pop(); + continue; + } + + stk.Pop(); + + var gc = tup.Item1.TransferCmd as GotoCmd; + if (gc.labelTargets.Count <= tup.Item2) + continue; + + stk.Push(Tuple.Create(tup.Item1, tup.Item2 + 1)); + stk.Push(Tuple.Create(gc.labelTargets[tup.Item2], 0)); + } + yield break; + } + + bool isHidden(Variable v) + { + return QKeyValue.FindBoolAttribute(v.Attributes, "hidden"); + } + + bool isVisible(Variable v) + { + return !isHidden(v); + } + + public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) + { + Debug.Assert(this.program == program); + + // Record current time + var startTime = DateTime.UtcNow; + + CommandLineOptions.Clo.ProverCCLimit = 1; + prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime); + + // Flush any axioms that came with the program before we start SI on this implementation + prover.AssertAxioms(); + + GenVc(impl, callback); + + prover.Check(); + var outcome = prover.CheckOutcomeCore(handler); + //var outcome = ProverInterface.Outcome.Valid; + + prover.Close(); + + + + //Console.WriteLine("Answer = {0}", outcome); + + return ProverInterfaceOutcomeToConditionGenerationOutcome(outcome); + } + } + } // namespace VC -- cgit v1.2.3