scyther/src/main.c

713 lines
14 KiB
C
Raw Normal View History

2004-05-15 16:26:21 +01:00
/**
*@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.
2004-05-15 16:45:08 +01:00
*
* \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
2004-05-15 16:45:08 +01:00
*
* 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.
2004-05-15 16:26:21 +01:00
*/
enum exittypes
{ EXIT_NOATTACK = 0, EXIT_ERROR = 1, EXIT_NOCLAIM = 2, EXIT_ATTACK = 3 };
2004-04-23 11:58:43 +01:00
#include <stdlib.h>
#include <stdio.h>
#include <time.h>
#include <limits.h>
#include "system.h"
2004-04-23 11:58:43 +01:00
#include "debug.h"
#include "modelchecker.h"
#include "memory.h"
#include "symbol.h"
2004-04-23 11:58:43 +01:00
#include "pheading.h"
#include "symbol.h"
#include "parser.h"
2004-04-23 11:58:43 +01:00
#include "tac.h"
#include "timer.h"
2004-04-23 11:58:43 +01:00
#include "compiler.h"
#include "latex.h"
#include "output.h"
2004-08-15 12:55:22 +01:00
#include "binding.h"
#include "switches.h"
#include "specialterm.h"
2004-04-23 11:58:43 +01:00
// The global system state
System sys;
2004-04-23 11:58:43 +01:00
extern struct tacnode *spdltac;
extern int mgu_match;
2004-04-23 11:58:43 +01:00
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 main body, as called by the environment.
2004-04-23 11:58:43 +01:00
int
main (int argc, char **argv)
{
int nerrors;
int exitcode = EXIT_NOATTACK;
2004-04-23 11:58:43 +01:00
/* Initialize memory routines */
memInit ();
/* initialize symbols */
termsInit ();
termmapsInit ();
2004-04-23 11:58:43 +01:00
termlistsInit ();
knowledgeInit ();
symbolsInit ();
tacInit ();
/*
* ------------------------------------------------
* generate system
* ------------------------------------------------
*/
/* process any command-line switches */
switchesInit (argc, argv);
/* start system */
sys = systemInit ();
/* init compiler for this system */
compilerInit (sys);
2004-04-23 11:58:43 +01:00
sys->know = emptyKnowledge ();
2004-04-23 11:58:43 +01:00
/* parse input */
yyparse ();
#ifdef DEBUG
if (DEBUGL (1))
tacPrint (spdltac);
#endif
/* compile */
if (switches.engine != ARACHNE_ENGINE)
{
// Compile as many runs as possible
compile (spdltac, switches.runs);
}
else
{
// Compile no runs for Arachne
compile (spdltac, 0);
}
2004-04-23 11:58:43 +01:00
scanner_cleanup ();
/* preprocess */
preprocess (sys);
2004-04-23 11:58:43 +01:00
#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 */
/*
* ---------------------------------------
* Switches consistency checking.
* ---------------------------------------
*/
/* Latex only makes sense for attacks */
if (switches.latex && switches.output != ATTACK)
{
error ("Scyther can only generate LaTeX output for attacks.");
}
#ifdef DEBUG
if (DEBUGL (4))
{
warning ("Selected output method is %i", switches.output);
}
#endif
if (switches.engine == ARACHNE_ENGINE)
{
arachneInit (sys);
}
/*
* ---------------------------------------
* Start real stuff
* ---------------------------------------
*/
2004-04-23 11:58:43 +01:00
/* xml init */
if (switches.xml)
xmlOutInit ();
2004-04-23 11:58:43 +01:00
/* latex header? */
if (switches.latex)
2004-04-23 11:58:43 +01:00
latexInit (sys, argc, argv);
/* model check system */
#ifdef DEBUG
if (DEBUGL (1))
warning ("Start modelchecking system.");
2004-04-23 11:58:43 +01:00
#endif
MC_single (sys);
2004-08-09 11:41:25 +01:00
/*
* ---------------------------------------
* After checking the system, results
* ---------------------------------------
*/
2004-04-23 11:58:43 +01:00
/* Display shortest attack, if any */
if (sys->attack != NULL && sys->attack->length != 0)
{
if (switches.output == ATTACK)
{
attackDisplay (sys);
}
/* mark exit code */
exitcode = EXIT_ATTACK;
}
else
{
2004-07-29 13:04:53 +01:00
/* 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)
2004-07-29 13:04:53 +01:00
{
/* mark exit code */
exitcode = EXIT_NOCLAIM;
2004-07-29 13:04:53 +01:00
}
cl_scan = cl_scan->next;
}
2004-07-29 13:04:53 +01:00
2004-04-23 11:58:43 +01:00
}
/* latex closeup */
if (switches.latex)
2004-04-23 11:58:43 +01:00
latexDone (sys);
/* xml closeup */
if (switches.xml)
xmlOutDone ();
/* Transfer any scenario counting to the exit code,
* assuming that there is no error. */
if (exitcode != EXIT_ERROR && switches.scenario < 0)
{
exitcode = sys->countScenario;
}
2004-04-23 11:58:43 +01:00
/*
* Now we clean up any memory that was allocated.
*/
if (switches.engine == ARACHNE_ENGINE)
{
arachneDone ();
2004-08-15 12:55:22 +01:00
bindingDone ();
}
2004-04-23 11:58:43 +01:00
knowledgeDestroy (sys->know);
systemDone (sys);
compilerDone ();
2004-04-23 11:58:43 +01:00
/* done symbols */
tacDone ();
symbolsDone ();
knowledgeDone ();
termlistsDone ();
termmapsDone ();
2004-04-23 11:58:43 +01:00
termsDone ();
/* memory clean up? */
strings_cleanup ();
memDone ();
exit:
return exitcode;
}
//! Display time and state space size information using ASCII.
/**
* Displays also whether an attack was found or not.
*/
2004-04-23 11:58:43 +01:00
void
timersPrint (const System sys)
{
2004-07-29 13:04:53 +01:00
Claimlist cl_scan;
int anyclaims;
2004-06-13 22:15:26 +01:00
// #define NOTIMERS
2004-04-23 11:58:43 +01:00
/* display stats */
if (switches.output != SUMMARY)
{
globalError++;
}
2004-04-23 11:58:43 +01:00
//**********************************************************************
2004-04-23 11:58:43 +01:00
/* states traversed */
if (switches.engine == POR_ENGINE)
{
eprintf ("states\t");
statesPrintShort (sys);
eprintf ("\n");
/* scenario info */
2004-04-23 11:58:43 +01:00
if (switches.scenario > 0)
{
eprintf ("scen_st\t");
statesFormat (sys->statesScenario);
eprintf ("\n");
}
/* flag
*
* L n Attack of length <n>
* None failed claim
* NoClaim no claims
*/
eprintf ("attack\t");
if (sys->claims == STATES0)
{
eprintf ("NoClaim\n");
}
2004-04-23 11:58:43 +01:00
else
{
if (sys->failed != STATES0)
eprintf ("L:%i\n", attackLength (sys->attack));
else
eprintf ("None\n");
}
2004-04-23 11:58:43 +01:00
#ifndef NOTIMERS
/* print time */
double seconds;
seconds = (double) clock () / CLOCKS_PER_SEC;
eprintf ("time\t%.3e\n", seconds);
/* states per second */
2004-04-23 11:58:43 +01:00
eprintf ("st/sec\t");
if (seconds > 0)
{
eprintf ("%.3e\n", statesDouble (sys->states) / seconds);
}
else
{
eprintf ("<inf>\n");
}
2004-05-26 13:17:09 +01:00
#endif
}
//**********************************************************************
2004-07-29 13:04:53 +01:00
/* 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 = false;
while (cl_scan != NULL)
2004-07-29 13:04:53 +01:00
{
if (!isTermEqual (cl_scan->type, CLAIM_Empty))
{
Protocol protocol;
Term pname;
Term rname;
Termlist labellist;
anyclaims = true;
eprintf ("claim\t");
protocol = (Protocol) cl_scan->protocol;
pname = protocol->nameterm;
rname = cl_scan->rolename;
labellist = tuple_to_termlist (cl_scan->label);
/* maybe the label contains duplicate info: if so, we remove it here */
{
Termlist tl;
tl = labellist;
while (tl != NULL)
{
if (isTermEqual (tl->term, pname)
|| isTermEqual (tl->term, rname))
{
tl = termlistDelTerm (tl);
labellist = tl;
}
else
{
tl = tl->next;
}
}
}
termPrint (pname);
eprintf (",");
termPrint (rname);
eprintf ("\t");
/* second print event_label */
termPrint (cl_scan->type);
eprintf ("_");
if (labellist != NULL)
{
Termlist tl;
tl = labellist;
while (tl != NULL)
{
termPrint (tl->term);
tl = tl->next;
if (tl != NULL)
{
eprintf (",");
}
}
/* clean up */
termlistDelete (labellist);
labellist = NULL;
}
else
{
eprintf ("?");
}
/* add parameter */
eprintf ("\t");
if (cl_scan->parameter != NULL)
{
termPrint (cl_scan->parameter);
}
2004-08-19 14:09:35 +01:00
else
{
eprintf ("-");
}
2005-12-27 12:24:12 +00:00
/* now report the status */
eprintf ("\t");
2005-12-27 12:24:12 +00:00
eprintf ("attacks: ");
if (cl_scan->count > 0 && cl_scan->failed > 0)
{
/* there is an attack */
if (!isTermEqual (cl_scan->type, CLAIM_Reachable))
{
/* a normal claim */
eprintf ("yes");
}
else
{
/* Reachable is not an attack */
eprintf ("no");
}
eprintf ("\t");
/* are these all attacks? */
eprintf ("[");
if (cl_scan->complete)
{
eprintf ("exactly");
}
else
{
eprintf ("at least");
}
eprintf (" %i variant", cl_scan->failed);
if (cl_scan->failed != 1)
{
eprintf ("s");
}
eprintf ("]");
2005-12-27 12:24:12 +00:00
}
else
{
2005-12-27 12:24:12 +00:00
/* no attack */
eprintf ("no\t");
/* subcases */
if (cl_scan->count == 0)
{
2005-12-27 12:24:12 +00:00
/* not encountered */
eprintf ("[does not occur]");
}
2004-08-19 14:09:35 +01:00
else
{
2005-12-27 12:24:12 +00:00
/* does occur */
if (cl_scan->complete)
{
2005-12-27 12:24:12 +00:00
/* complete proof */
eprintf ("[proof of correctness]");
}
else
{
2005-12-27 12:24:12 +00:00
/* only due to bounds */
eprintf ("[no attack within bounds]");
if (cl_scan->timebound)
eprintf ("\ttime=%i", get_time_limit ());
}
}
2004-08-19 14:09:35 +01:00
}
2005-12-27 12:24:12 +00:00
2005-12-27 13:44:12 +00:00
/* any warnings */
if (cl_scan->warnings)
{
eprintf ("\t[read the warnings for more information]");
2005-12-27 13:44:12 +00:00
}
2005-12-27 12:24:12 +00:00
/* proceed to next claim */
eprintf ("\n");
2004-07-29 13:04:53 +01:00
}
cl_scan = cl_scan->next;
}
if (!anyclaims)
{
warning ("No claims in system.");
}
/* reset globalError */
if (switches.output != SUMMARY)
{
globalError--;
2004-07-29 13:04:53 +01:00
}
2004-04-23 11:58:43 +01:00
}
//! Analyse the model by incremental runs.
2004-04-23 11:58:43 +01:00
/*
* 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);
2004-04-23 11:58:43 +01:00
res = modelCheck (sys);
fprintf (stderr, "\n");
2004-04-23 11:58:43 +01:00
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 (switches.prune != 0)
2004-04-23 11:58:43 +01:00
{
flag = 0;
}
}
runs++;
}
while (flag && runs <= maxruns);
sys->maxruns = maxruns;
2004-04-23 11:58:43 +01:00
}
//! 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.
*/
2004-04-23 11:58:43 +01:00
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;
2004-05-26 09:52:15 +01:00
int flag;
int res;
2004-04-23 11:58:43 +01:00
tracestep = 3; /* what is a sensible stepping size? */
2004-05-26 13:17:09 +01:00
flag = 1;
2004-04-23 11:58:43 +01:00
maxtracelen = getMaxTraceLength (sys);
tracelen = maxtracelen - tracestep;
while (tracelen > 6) /* what is a reasonable minimum? */
tracelen -= tracestep;
2004-05-26 09:52:15 +01:00
flag = 1;
2004-04-23 11:58:43 +01:00
do
{
systemReset (sys);
sys->maxtracelength = tracelen;
systemRuns (sys);
fprintf (stderr,
"%i of %i trace length in incremental trace length search.\n",
tracelen, maxtracelen);
2004-04-23 11:58:43 +01:00
res = modelCheck (sys);
fprintf (stderr, "\n");
2004-04-23 11:58:43 +01:00
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 (switches.prune != 0)
2004-04-23 11:58:43 +01:00
{
flag = 0;
}
}
tracelen += tracestep;
}
while (flag && tracelen <= maxtracelen);
}
//! Analyse the model with a fixed scenario.
/**
* Traditional handywork.
2004-04-23 11:58:43 +01:00
*/
void
MC_single (const System sys)
{
/*
* simple one-time check
*/
systemReset (sys); // reset any globals
systemRuns (sys); // init runs data
2004-04-23 11:58:43 +01:00
modelCheck (sys);
}
//! Model check the system, given all parameters.
2004-04-23 11:58:43 +01:00
/*
* Precondition: the system was reset with the corresponding parameters.
2004-05-15 16:26:21 +01:00
* 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.
2004-04-23 11:58:43 +01:00
*/
int
modelCheck (const System sys)
{
if (switches.output == STATESPACE)
{
graphInit (sys);
}
/* modelcheck the system */
switch (switches.engine)
2004-08-11 10:51:17 +01:00
{
case POR_ENGINE:
if (sys->maxruns > 0)
traverse (sys);
else
warning ("Model checking system with empty scenario.");
2004-08-11 10:51:17 +01:00
break;
case ARACHNE_ENGINE:
arachne ();
2004-08-11 10:51:17 +01:00
break;
default:
error ("Unknown engine type %i.", switches.engine);
2004-08-11 10:51:17 +01:00
}
/* clean up any states display */
if (switches.reportStates > 0)
{
// States: 1.000e+06
fprintf (stderr, " \r");
}
timersPrint (sys);
if (switches.output == STATESPACE)
{
graphDone (sys);
}
if (switches.scenario > 0)
{
/* Traversing a scenario. Maybe we ran out. */
if (switches.scenario > sys->countScenario)
{
/* Signal as error */
exit (1);
}
}
return (sys->failed != STATES0);
2004-04-23 11:58:43 +01:00
}