/** *@file main.c * \brief The main file. * * Contains the main switch handling, and passes everything to the core logic. */ /** * \mainpage * * \section intro Introduction * * Scyther is a model checker for security protocols. * * \section install Installation * * How to install Scyther. * * \section exit Exit codes * * 0 Okay No attack found, claims encountered * * 1 Error Something went wrong (error) E.g. switch error, or scenario ran out. * * 2 Okay No attack found (because) no claims encountered * * 3 Okay Attack found * * However, if the --scenario=-1 switch is used, the exit code is used to return the number of scenarios. * * \section coding Coding conventions * * Usually, each source file except main.c has an myfileInit() and myfileDone() function * available. These allow any initialisation and destruction of required structures. * * GNU indent rules are used, but K&R derivatives are allowed as well. Conversion can * be done for any style using the GNU indent program. */ enum exittypes { EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_NOCLAIM = 2, EXIT_ATTACK = 3 }; #include #include #include #include #include "system.h" #include "debug.h" #include "modelchecker.h" #include "memory.h" #include "symbol.h" #include "pheading.h" #include "symbol.h" #include "parser.h" #include "tac.h" #include "timer.h" #include "compiler.h" #include "latex.h" #include "output.h" #include "binding.h" #include "version.h" #include "argtable2.h" // The global system state System sys; extern struct tacnode *spdltac; extern Term TERM_Claim; extern int mgu_match; void scanner_cleanup (void); void strings_cleanup (void); int yyparse (void); void MC_incRuns (const System sys); void MC_incTraces (const System sys); void MC_single (const System sys); int modelCheck (const System sys); //! The name of this program. const char *progname = "scyther"; //! Release tag name. /** * Note that this is only referenced in the help output of the commandline program. * \todo Come up with a useful solution for release names. */ const char *releasetag = SVNVERSION; //! The number of seconds a test is allowed to run static int time_limit_seconds; //! The main body, as called by the environment. int main (int argc, char **argv) { struct arg_file *infile = arg_file0 (NULL, NULL, "FILE", "input file ('-' for stdin)"); struct arg_file *outfile = arg_file0 ("o", "output", "FILE", "output file (default is stdout)"); struct arg_lit *switch_arachne = arg_lit0 ("a", "arachne", "use Arachne engine"); struct arg_lit *switch_proof = arg_lit0 ("P", "proof", "generate proof output"); struct arg_str *switch_check = arg_str0 (NULL, "check", "CLAIM", "claim type to check (default is all)"); struct arg_int *switch_scenario = arg_int0 ("s", "scenario", NULL, "select a scenario instance 1-n (-1 to count)"); struct arg_int *switch_scenario_size = arg_int0 ("S", "scenario-size", NULL, "scenario size (fixed trace prefix length)"); struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL, "set traversal method, partial order reduction (default is 12)"); struct arg_int *switch_match_method = arg_int0 ("m", "match", NULL, "matching method (default is 0)"); struct arg_lit *switch_clp = arg_lit0 ("c", "cl", "use constraint logic, non-associative"); struct arg_int *switch_pruning_method = arg_int0 ("p", "prune", NULL, "pruning method (default is 2)"); struct arg_int *switch_prune_trace_length = arg_int0 ("l", "max-length", NULL, "prune traces longer than events."); struct arg_int *switch_prune_proof_depth = arg_int0 ("d", "max-depth", NULL, "prune proof deeper than splits."); struct arg_lit *switch_incremental_trace_length = arg_lit0 (NULL, "increment-traces", "incremental search using the length of the traces."); struct arg_int *switch_maximum_runs = arg_int0 ("r", "max-runs", NULL, "create at most runs"); struct arg_lit *switch_incremental_runs = arg_lit0 (NULL, "increment-runs", "incremental search using the number of runs"); struct arg_int *switch_goal_select_method = arg_int0 (NULL, "goal-select", NULL, "use goal selection method (default 3)"); struct arg_lit *switch_latex_output = arg_lit0 (NULL, "latex", "output attacks in LaTeX format"); struct arg_lit *switch_empty = arg_lit0 ("e", "empty", "do not generate output"); struct arg_lit *switch_progress_bar = arg_lit0 ("b", "progress-bar", "show progress bar"); struct arg_lit *switch_state_space_graph = arg_lit0 (NULL, "state-space", "output state space graph"); struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose", "allow implicit choose events (useful for few runs)"); struct arg_lit *switch_choose_first = arg_lit0 (NULL, "choose-first", "priority to any choose events"); struct arg_lit *switch_enable_read_symmetries = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions"); struct arg_lit *switch_disable_agent_symmetries = arg_lit0 (NULL, "no-agent-symm", "disable agent symmetry reductions"); struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions"); struct arg_lit *switch_disable_noclaims_reductions = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions"); struct arg_lit *switch_disable_endgame_reductions = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions"); struct arg_lit *switch_disable_claim_symmetry = arg_lit0 (NULL, "no-claimsymmetry-red", "disable claim symmetry reductions"); struct arg_lit *switch_summary = arg_lit0 (NULL, "summary", "show summary on stdout instead of stderr"); struct arg_lit *switch_echo = arg_lit0 ("E", "echo", "echo command line to stdout"); struct arg_int *switch_timer = arg_int0 ("T", "timer", NULL, "maximum time in seconds"); #ifdef DEBUG struct arg_int *switch_por_parameter = arg_int0 (NULL, "pp", NULL, "POR parameter"); struct arg_lit *switch_debug_indent = arg_lit0 ("I", "debug-indent", "indent the debug output using trace length"); struct arg_int *switch_debug_level = arg_int0 ("D", "debug", NULL, "set debug level (default is 0)"); #endif struct arg_lit *help = arg_lit0 (NULL, "help", "print this help and exit"); struct arg_lit *version = arg_lit0 (NULL, "version", "print version information and exit"); struct arg_end *end = arg_end (30); void *argtable[] = { infile, outfile, switch_empty, switch_proof, switch_state_space_graph, switch_scenario, switch_scenario_size, switch_latex_output, switch_summary, switch_echo, switch_progress_bar, switch_arachne, switch_check, switch_traversal_method, switch_match_method, switch_clp, switch_timer, switch_pruning_method, switch_prune_proof_depth, switch_prune_trace_length, switch_incremental_trace_length, switch_maximum_runs, switch_incremental_runs, switch_goal_select_method, switch_implicit_choose, switch_choose_first, switch_enable_read_symmetries, switch_enable_symmetry_order, switch_disable_agent_symmetries, switch_disable_noclaims_reductions, switch_disable_endgame_reductions, switch_disable_claim_symmetry, #ifdef DEBUG switch_por_parameter, switch_debug_indent, switch_debug_level, #endif help, version, end }; int nerrors; int exitcode = EXIT_NOATTACK; /* verify the argtable[] entries were allocated sucessfully */ if (arg_nullcheck (argtable) != 0) { /* NULL entries were detected, some allocations must have failed */ fprintf (stderr, "%s: insufficient memory\n", progname); exitcode = EXIT_ERROR; goto exit; } /* defaults * set any command line default values prior to parsing */ #ifdef DEBUG switch_debug_level->ival[0] = 0; switch_por_parameter->ival[0] = 0; #endif switch_scenario->ival[0] = 0; switch_scenario_size->ival[0] = 0; switch_traversal_method->ival[0] = 12; switch_match_method->ival[0] = 0; switch_prune_trace_length->ival[0] = -1; switch_prune_proof_depth->ival[0] = -1; switch_maximum_runs->ival[0] = INT_MAX; switch_pruning_method->ival[0] = 2; switch_goal_select_method->ival[0] = -1; switch_timer->ival[0] = 0; /* Parse the command line as defined by argtable[] */ nerrors = arg_parse (argc, argv, argtable); /* special case: '--help' takes precedence over error reporting */ if (help->count > 0) { printf ("Usage: %s ", progname); arg_print_syntax (stdout, argtable, "\n"); printf ("This program can model check security protocols for various\n"); printf ("properties, given a finite scenario.\n\n"); arg_print_glossary (stdout, argtable, " %-25s %s\n"); exitcode = 0; goto exit; } /* special case: '--version' takes precedence error reporting */ if (version->count > 0) { printf ("'%s' model checker for security protocols.\n", progname); #ifdef DEBUG printf ("Revision %s, compiled with debugging support.\n", releasetag); #else printf ("Revision %s\n", releasetag); #endif printf ("December 2003--, Cas Cremers\n"); exitcode = 0; goto exit; } /* If the parser returned any errors then display them and exit */ if (nerrors > 0) { /* Display the error details contained in the arg_end struct. */ arg_print_errors (stdout, end, progname); printf ("Try '%s --help' for more information.\n", progname); exitcode = EXIT_ERROR; goto exit; } /* special case: uname with no command line options induces brief help */ if (argc == 1) { printf ("Try '%s --help' for more information.\n", progname); exitcode = 0; goto exit; } /* * Arguments have been parsed by argtable, * continue with main code. */ /* Lutger-tries-to-test-with-broken-methods detector */ if (switch_clp->count > 0) { fprintf (stderr, "For the time being, this method is not supported, \n"); fprintf (stderr, "as too many changes have been made to the normal \n"); fprintf (stderr, "matching logic, and CL simply isn't reliable in \nmany "); fprintf (stderr, "ways. Try again in a few weeks.\n"); exit (0); } /* redirect in- and output according to supplied filenames */ /* output */ if (outfile->count > 0) { /* try to open */ if (!freopen (outfile->filename[0], "w", stdout)) { fprintf (stderr, "Could not create output file '%s'.\n", outfile->filename[0]); exit (1); } } /* input */ if (infile->count > 0) { /* check for the single dash */ if (strcmp (infile->filename[0], "-")) { if (!freopen (infile->filename[0], "r", stdin)) { fprintf (stderr, "Could not open input file '%s'.\n", infile->filename[0]); exit (1); } } } /* handle debug level */ #ifdef DEBUG debugSet (switch_debug_level->ival[0]); #else debugSet (0); #endif /* Initialize memory routines */ memInit (); /* initialize symbols */ termsInit (); termmapsInit (); termlistsInit (); knowledgeInit (); symbolsInit (); tacInit (); /* * ------------------------------------------------ * generate system * ------------------------------------------------ */ sys = systemInit (); if (switch_arachne->count > 0) { sys->engine = ARACHNE_ENGINE; bindingInit (sys); } /* init compiler for this system */ compilerInit (sys); /* transfer command line */ sys->argc = argc; sys->argv = argv; if (switch_echo->count > 0) { /* print command line */ fprintf (stdout, "command\t"); commandlinePrint (stdout, sys); fprintf (stdout, "\n"); } /* handle switches */ sys->switchRuns = switch_maximum_runs->ival[0]; /* maximum number of runs */ if (switch_implicit_choose->count > 0) /* allow implicit chooses */ sys->switchForceChoose = 0; if (switch_choose_first->count > 0) sys->switchChooseFirst = 1; /* priority to chooses */ if (switch_enable_read_symmetries->count > 0) { if (switch_enable_symmetry_order->count > 0) error ("--read-symm and --symm-order cannot be used at the same time."); sys->switchReadSymm = 1; } if (switch_enable_symmetry_order->count > 0) sys->switchSymmOrder = 1; /* enable symmetry order */ if (switch_disable_agent_symmetries->count > 0) sys->switchAgentSymm = 0; /* disable agent symmetry order */ if (switch_disable_noclaims_reductions->count > 0) sys->switchNomoreClaims = 0; /* disable no more claims cutter */ if (switch_disable_endgame_reductions->count > 0) sys->switchReduceEndgame = 0; /* disable endgame cutter */ if (switch_disable_claim_symmetry->count > 0) sys->switchReduceClaims = 0; /* disable claim symmetry cutter */ if (switch_summary->count > 0) sys->output = SUMMARY; /* report summary on stdout */ if (switch_proof->count > 0) sys->output = PROOF; /* report proof on stdout (for arachne only) */ /* * The scenario selector has an important side effect; when it is non-null, * any scenario traversing selects chooses first. */ sys->switchScenario = switch_scenario->ival[0]; /* scenario selector */ sys->switchScenarioSize = switch_scenario_size->ival[0]; /* scenario size */ if (sys->switchScenario == 0 && sys->switchScenarioSize > 0) { /* no scenario, but a size is set. so override */ #ifdef DEBUG warning ("Scanning scenarios."); #endif sys->switchScenario = -1; } if (sys->switchScenario < 0) { sys->output = SCENARIOS; } if (sys->switchScenario != 0 && sys->switchScenarioSize == 0) { #ifdef DEBUG warning ("Scenario selection without trace prefix length implies --choose-first."); #endif sys->switchChooseFirst = 1; } #ifdef DEBUG sys->porparam = switch_por_parameter->ival[0]; #endif sys->latex = switch_latex_output->count; sys->know = emptyKnowledge (); /* parse compiler-dependant switches */ if (switch_check->count > 0) { Term claim; #ifdef DEBUG if (lookup (switch_check->sval[0]) == NULL) { globalError++; warning ("Could not find this string at all in:"); symbolPrintAll (); eprintf ("\n"); globalError--; } #endif claim = findGlobalConstant (switch_check->sval[0]); if (claim == NULL) error ("Unknown claim type to check."); if (inTermlist (claim->stype, TERM_Claim)) sys->switchClaimToCheck = claim; else error ("Claim type to check is not a claim."); } /* parse input */ yyparse (); #ifdef DEBUG if (DEBUGL (1)) tacPrint (spdltac); #endif /* compile */ if (sys->engine != ARACHNE_ENGINE) { // Compile as many runs as possible compile (spdltac, switch_maximum_runs->ival[0]); } else { // Compile no runs for Arachne compile (spdltac, 0); } scanner_cleanup (); /* preprocess */ preprocess (sys); #ifdef DEBUG if (DEBUGL (1)) { printf ("\nCompilation yields:\n\n"); printf ("untrusted agents: "); termlistPrint (sys->untrusted); printf ("\n"); knowledgePrint (sys->know); printf ("inverses: "); knowledgeInversesPrint (sys->know); printf ("\n"); locVarPrint (sys->locals); protocolsPrint (sys->protocols); printf ("\nInstantiated runs:\n\n"); runsPrint (sys); } #endif /* allocate memory for traces, based on runs */ systemStart (sys); sys->traceKnow[0] = sys->know; // store initial knowledge /* add parameters to system */ sys->clp = (switch_clp->count > 0 ? 1 : 0); sys->traverse = switch_traversal_method->ival[0]; sys->match = switch_match_method->ival[0]; mgu_match = sys->match; sys->prune = switch_pruning_method->ival[0]; time_limit_seconds = switch_timer->ival[0]; set_time_limit (switch_timer->ival[0]); if (switch_progress_bar->count > 0) /* enable progress display */ sys->switchS = 50000; else /* disable progress display */ sys->switchS = 0; if (switch_state_space_graph->count > 0) { /* enable state space graph output */ sys->output = STATESPACE; //!< New method } if (switch_empty->count > 0) sys->output = EMPTY; if (switch_prune_proof_depth->ival[0] >= 0) sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0]; if (switch_prune_trace_length->ival[0] >= 0) sys->switch_maxtracelength = switch_prune_trace_length->ival[0]; if (switch_goal_select_method->ival[0] >= 0) sys->switchGoalSelectMethod = switch_goal_select_method->ival[0]; #ifdef DEBUG /* in debugging mode, some extra switches */ if (switch_debug_indent->count > 0) indentActivate (); if (DEBUGL (1)) printf ("Using traversal method %i.\n", sys->traverse); #else /* non-debug defaults */ sys->switchM = 0; #endif /* * --------------------------------------- * Switches consistency checking. * --------------------------------------- */ /* Latex only makes sense for attacks */ if (sys->latex && sys->output != ATTACK) { error ("Scyther can only generate LaTeX output for attacks."); } /* Incremental stuff only works for attack locating */ if (switch_incremental_runs->count > 0 || switch_incremental_trace_length->count > 0) { if (sys->output != ATTACK && sys->output != EMPTY) { error ("Incremental traversal only for empty or attack output."); } } #ifdef DEBUG if (DEBUGL (4)) { warning ("Selected output method is %i", sys->output); } #endif if (sys->engine == ARACHNE_ENGINE) { arachneInit (sys); } /* * --------------------------------------- * Start real stuff * --------------------------------------- */ /* latex header? */ if (sys->latex) latexInit (sys, argc, argv); /* model check system */ #ifdef DEBUG if (DEBUGL (1)) warning ("Start modelchecking system."); #endif if (switch_incremental_runs->count > 0) { MC_incRuns (sys); } else { if (switch_incremental_trace_length->count > 0) { MC_incTraces (sys); } else { MC_single (sys); } } /* * --------------------------------------- * After checking the system, results * --------------------------------------- */ /* Display shortest attack, if any */ if (sys->attack != NULL && sys->attack->length != 0) { if (sys->output == ATTACK) { attackDisplay (sys); } /* mark exit code */ exitcode = EXIT_ATTACK; } else { /* check if there is a claim type that was never reached */ Claimlist cl_scan; cl_scan = sys->claimlist; while (cl_scan != NULL) { if (cl_scan->failed == STATES0) { /* mark exit code */ exitcode = EXIT_NOCLAIM; } cl_scan = cl_scan->next; } } /* latex closeup */ if (sys->latex) latexDone (sys); /* Transfer any scenario counting to the exit code, * assuming that there is no error. */ if (exitcode != EXIT_ERROR && sys->switchScenario < 0) { exitcode = sys->countScenario; } /* * Now we clean up any memory that was allocated. */ if (sys->engine == ARACHNE_ENGINE) { arachneDone (); bindingDone (); } knowledgeDestroy (sys->know); systemDone (sys); compilerDone (); /* done symbols */ tacDone (); symbolsDone (); knowledgeDone (); termlistsDone (); termmapsDone (); termsDone (); /* memory clean up? */ strings_cleanup (); memDone (); exit: /* deallocate each non-null entry in argtable[] */ arg_free (argtable); return exitcode; } //! Display time and state space size information using ASCII. /** * Displays also whether an attack was found or not. */ void timersPrint (const System sys) { Claimlist cl_scan; int anyclaims; // #define NOTIMERS /* display stats */ if (sys->output != SUMMARY) { globalError++; } /* states traversed */ eprintf ("states\t"); statesPrintShort (sys); eprintf ("\n"); /* scenario info */ if (sys->switchScenario > 0) { eprintf ("scen_st\t"); statesFormat (sys->statesScenario); eprintf ("\n"); } /* flag * * L n Attack of length * None failed claim * NoClaim no claims */ eprintf ("attack\t"); if (sys->claims == STATES0) { eprintf ("NoClaim\n"); } else { if (sys->failed != STATES0) eprintf ("L:%i\n", attackLength (sys->attack)); else eprintf ("None\n"); } #ifndef NOTIMERS /* print time */ double seconds; seconds = (double) clock () / CLOCKS_PER_SEC; eprintf ("time\t%.3e\n", seconds); /* states per second */ eprintf ("st/sec\t"); if (seconds > 0) { eprintf ("%.3e\n", statesDouble (sys->states) / seconds); } else { eprintf ("\n"); } #endif /* Print also individual claims */ /* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing) */ cl_scan = sys->claimlist; anyclaims = 0; while (cl_scan != NULL) { anyclaims = 1; eprintf ("claim\t"); /* claim label is tuple */ if (realTermTuple (cl_scan->label)) { /* modern version: claim label is tuple (protocname, label) */ /* first print protocol.role */ termPrint (TermOp1 (cl_scan->label)); eprintf ("\t"); termPrint (cl_scan->rolename); eprintf ("\t"); /* second print event_label */ termPrint (cl_scan->type); eprintf ("_"); termPrint (TermOp2 (cl_scan->label)); eprintf ("\t"); } else { /* old-fashioned output */ termPrint (cl_scan->type); eprintf ("\t"); termPrint (cl_scan->rolename); eprintf (" ("); termPrint (cl_scan->label); eprintf (")\t"); } /* print counts etc. */ eprintf ("found:\t"); statesFormat (cl_scan->count); if (cl_scan->count > 0) { if (cl_scan->failed > 0) { eprintf ("\t"); eprintf ("failed:\t"); statesFormat (cl_scan->failed); } else { eprintf ("\tcorrect: "); if (cl_scan->complete) { eprintf ("complete_proof"); } else { eprintf ("bounded_proof"); if (cl_scan->timebound) eprintf ("\ttime=%i", time_limit_seconds); } } } else { eprintf ("\tcorrect: does_not_occur"); } eprintf ("\n"); cl_scan = cl_scan->next; } if (!anyclaims) { warning ("No claims in system."); } /* reset globalError */ if (sys->output != SUMMARY) { globalError--; } } //! Analyse the model by incremental runs. /* * This procedure considers mainly incremental searches, and settings * parameters for that. The real work is handled by modelCheck. */ void MC_incRuns (const System sys) { /* * incremental runs check * * note: we assume that at least one run needs to be checked. */ int maxruns = sys->maxruns; int runs = 1; int flag = 1; int res; do { systemReset (sys); sys->maxruns = runs; systemRuns (sys); fprintf (stderr, "%i of %i runs in incremental runs search.\n", runs, maxruns); res = modelCheck (sys); fprintf (stderr, "\n"); if (res) { /* Apparently a violation occurred. If we are searching * the whole space, then we just continue. However, if * we're looking to prune, ``the buck stops here''. */ if (sys->prune != 0) { flag = 0; } } runs++; } while (flag && runs <= maxruns); sys->maxruns = maxruns; } //! Analyse the model by incremental trace lengths. /* * This procedure considers mainly incremental searches, and settings * parameters for that. The real work is handled by modelCheck. */ void MC_incTraces (const System sys) { /* * incremental traces check * * note: we assume that at least one run needs to be checked. */ int maxtracelen; int tracelen; int tracestep; int flag; int res; tracestep = 3; /* what is a sensible stepping size? */ flag = 1; maxtracelen = getMaxTraceLength (sys); tracelen = maxtracelen - tracestep; while (tracelen > 6) /* what is a reasonable minimum? */ tracelen -= tracestep; flag = 1; do { systemReset (sys); sys->maxtracelength = tracelen; systemRuns (sys); fprintf (stderr, "%i of %i trace length in incremental trace length search.\n", tracelen, maxtracelen); res = modelCheck (sys); fprintf (stderr, "\n"); if (res) { /* Apparently a violation occurred. If we are searching * the whole space, then we just continue. However, if * we're looking to prune, ``the buck stops here''. */ if (sys->prune != 0) { flag = 0; } } tracelen += tracestep; } while (flag && tracelen <= maxtracelen); } //! Analyse the model with a fixed scenario. /** * Traditional handywork. */ void MC_single (const System sys) { /* * simple one-time check */ systemReset (sys); // reset any globals systemRuns (sys); // init runs data modelCheck (sys); } //! Model check the system, given all parameters. /* * Precondition: the system was reset with the corresponding parameters. * Reports time and states traversed. * Note that the return values doubles as the number of failed claims. *@return True iff any claim failed, and thus an attack was found. */ int modelCheck (const System sys) { if (sys->output == STATESPACE) { graphInit (sys); } /* modelcheck the system */ switch (sys->engine) { case POR_ENGINE: traverse (sys); break; case ARACHNE_ENGINE: arachne (); break; default: error ("Unknown engine type %i.", sys->engine); } /* clean up any states display */ if (sys->switchS > 0) { // States: 1.000e+06 fprintf (stderr, " \r"); } timersPrint (sys); if (sys->output == STATESPACE) { graphDone (sys); } if (sys->switchScenario > 0) { /* Traversing a scenario. Maybe we ran out. */ if (sys->switchScenario > sys->countScenario) { /* Signal as error */ exit (1); } } return (sys->failed != STATES0); }