5487d3ae90
method. A big cleanup has been started, but is not finished yet, so minor artefacts might still remain. These are to be cleaned up later.
504 lines
9.5 KiB
C
504 lines
9.5 KiB
C
/**
|
|
*@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
|
|
*
|
|
* \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.
|
|
*/
|
|
|
|
#include <stdlib.h>
|
|
#include <stdio.h>
|
|
#include <time.h>
|
|
#include <limits.h>
|
|
#include "system.h"
|
|
#include "debug.h"
|
|
#include "symbol.h"
|
|
#include "pheading.h"
|
|
#include "symbol.h"
|
|
#include "parser.h"
|
|
#include "tac.h"
|
|
#include "timer.h"
|
|
#include "compiler.h"
|
|
#include "binding.h"
|
|
#include "switches.h"
|
|
#include "specialterm.h"
|
|
#include "color.h"
|
|
#include "error.h"
|
|
|
|
//! The global system state pointer
|
|
System sys;
|
|
|
|
//! Pointer to the tac node container
|
|
extern struct tacnode *spdltac;
|
|
//! Match mode
|
|
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 main body, as called by the environment.
|
|
int
|
|
main (int argc, char **argv)
|
|
{
|
|
int nerrors;
|
|
int exitcode = EXIT_NOATTACK;
|
|
|
|
/* initialize symbols */
|
|
termsInit ();
|
|
termmapsInit ();
|
|
termlistsInit ();
|
|
knowledgeInit ();
|
|
symbolsInit ();
|
|
tacInit ();
|
|
|
|
/*
|
|
* ------------------------------------------------
|
|
* generate system
|
|
* ------------------------------------------------
|
|
*/
|
|
|
|
/* process any command-line switches */
|
|
switchesInit (argc, argv);
|
|
|
|
/* process colors */
|
|
colorInit ();
|
|
|
|
/* start system */
|
|
sys = systemInit ();
|
|
|
|
/* init compiler for this system */
|
|
compilerInit (sys);
|
|
|
|
sys->know = emptyKnowledge ();
|
|
|
|
|
|
/* parse input */
|
|
|
|
yyparse ();
|
|
#ifdef DEBUG
|
|
if (DEBUGL (1))
|
|
tacPrint (spdltac);
|
|
#endif
|
|
|
|
/* compile */
|
|
|
|
// 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 */
|
|
|
|
|
|
/*
|
|
* ---------------------------------------
|
|
* Switches consistency checking.
|
|
* ---------------------------------------
|
|
*/
|
|
|
|
#ifdef DEBUG
|
|
if (DEBUGL (4))
|
|
{
|
|
warning ("Selected output method is %i", switches.output);
|
|
}
|
|
#endif
|
|
|
|
arachneInit (sys);
|
|
|
|
/*
|
|
* ---------------------------------------
|
|
* Start real stuff
|
|
* ---------------------------------------
|
|
*/
|
|
|
|
/* xml init */
|
|
if (switches.xml)
|
|
xmlOutInit ();
|
|
|
|
/* model check system */
|
|
#ifdef DEBUG
|
|
if (DEBUGL (1))
|
|
warning ("Start modelchecking system.");
|
|
#endif
|
|
MC_single (sys);
|
|
|
|
/*
|
|
* ---------------------------------------
|
|
* After checking the system, results
|
|
* ---------------------------------------
|
|
*/
|
|
|
|
/* Exitcodes are *not* correct anymore */
|
|
|
|
exitcode = EXIT_ATTACK;
|
|
|
|
/* xml closeup */
|
|
if (switches.xml)
|
|
xmlOutDone ();
|
|
|
|
/*
|
|
* Now we clean up any memory that was allocated.
|
|
*/
|
|
|
|
arachneDone ();
|
|
knowledgeDestroy (sys->know);
|
|
systemDone (sys);
|
|
colorDone ();
|
|
compilerDone ();
|
|
|
|
/* done symbols */
|
|
tacDone ();
|
|
symbolsDone ();
|
|
knowledgeDone ();
|
|
termlistsDone ();
|
|
termmapsDone ();
|
|
termsDone ();
|
|
|
|
/* memory clean up? */
|
|
strings_cleanup ();
|
|
|
|
exit:
|
|
return exitcode;
|
|
}
|
|
|
|
//! Print something bad
|
|
void
|
|
printBad (char *s)
|
|
{
|
|
eprintf ("%s%s%s", COLOR_Red, s, COLOR_Reset);
|
|
}
|
|
|
|
//! Print something good
|
|
void
|
|
printGood (char *s)
|
|
{
|
|
eprintf ("%s%s%s", COLOR_Green, s, COLOR_Reset);
|
|
}
|
|
|
|
//! Print state (existState, isAttack)
|
|
/**
|
|
* Fail == ( existState xor isAttack )
|
|
*/
|
|
void
|
|
printOkFail (int existState, int isAttack)
|
|
{
|
|
if (existState != isAttack)
|
|
{
|
|
printGood ("Ok");
|
|
}
|
|
else
|
|
{
|
|
printBad ("Fail");
|
|
}
|
|
}
|
|
|
|
//! 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 (switches.output != SUMMARY)
|
|
{
|
|
globalError++;
|
|
}
|
|
|
|
//**********************************************************************
|
|
|
|
/* 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)
|
|
{
|
|
if (!isTermEqual (cl_scan->type, CLAIM_Empty))
|
|
{
|
|
Protocol protocol;
|
|
Term pname;
|
|
Term rname;
|
|
Termlist labellist;
|
|
int isAttack; // stores whether this claim failure constitutes an attack or not
|
|
|
|
if (isTermEqual (cl_scan->type, CLAIM_Reachable))
|
|
{
|
|
// An attack on reachable is not really an attack, we're just generating the state space
|
|
isAttack = false;
|
|
}
|
|
else
|
|
{
|
|
isAttack = true;
|
|
}
|
|
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);
|
|
}
|
|
else
|
|
{
|
|
eprintf ("-");
|
|
}
|
|
|
|
/* now report the status */
|
|
eprintf ("\t");
|
|
if (cl_scan->count > 0 && cl_scan->failed > 0)
|
|
{
|
|
/* there is a state */
|
|
printOkFail (true, isAttack);
|
|
|
|
eprintf ("\t");
|
|
/* are these all attacks? */
|
|
eprintf ("[");
|
|
if (cl_scan->complete)
|
|
{
|
|
eprintf ("exactly");
|
|
}
|
|
else
|
|
{
|
|
eprintf ("at least");
|
|
}
|
|
eprintf (" %i ", cl_scan->failed);
|
|
if (isAttack)
|
|
{
|
|
eprintf ("attack");
|
|
}
|
|
else
|
|
{
|
|
eprintf ("variant");
|
|
}
|
|
if (cl_scan->failed != 1)
|
|
{
|
|
eprintf ("s");
|
|
}
|
|
eprintf ("]");
|
|
}
|
|
else
|
|
{
|
|
/* no state */
|
|
printOkFail (false, isAttack);
|
|
eprintf ("\t");
|
|
|
|
/* subcases */
|
|
if (cl_scan->count == 0)
|
|
{
|
|
/* not encountered */
|
|
eprintf ("[does not occur]");
|
|
}
|
|
else
|
|
{
|
|
/* does occur */
|
|
if (cl_scan->complete)
|
|
{
|
|
/* complete proof */
|
|
eprintf ("[proof of correctness]");
|
|
}
|
|
else
|
|
{
|
|
/* only due to bounds */
|
|
eprintf ("[no attack within bounds]");
|
|
}
|
|
}
|
|
if (cl_scan->timebound)
|
|
eprintf ("\ttime=%i", get_time_limit ());
|
|
}
|
|
|
|
/* states (if asked) */
|
|
if (switches.countStates)
|
|
{
|
|
eprintf ("\tstates=");
|
|
statesFormat (cl_scan->states);
|
|
}
|
|
|
|
/* any warnings */
|
|
if (cl_scan->warnings)
|
|
{
|
|
eprintf ("\t[read the warnings for more information]");
|
|
}
|
|
|
|
/* proceed to next claim */
|
|
eprintf ("\n");
|
|
}
|
|
cl_scan = cl_scan->next;
|
|
}
|
|
if (!anyclaims)
|
|
{
|
|
warning ("No claims in system.");
|
|
}
|
|
|
|
/* reset globalError */
|
|
if (switches.output != SUMMARY)
|
|
{
|
|
globalError--;
|
|
}
|
|
}
|
|
|
|
//! Analyse the model
|
|
/**
|
|
* 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)
|
|
{
|
|
/* modelcheck the system */
|
|
arachne ();
|
|
|
|
/* clean up any states display */
|
|
if (switches.reportStates > 0)
|
|
{
|
|
// States: 1.000e+06
|
|
fprintf (stderr, " \r");
|
|
}
|
|
|
|
timersPrint (sys);
|
|
return (sys->failed != STATES0);
|
|
}
|