- Added preliminary support for singular attack output.
This commit is contained in:
ccremers
parent
ff503b24af
commit
c20810def5
117
src/arachne.c
117
src/arachne.c
|
|
@ -53,6 +53,7 @@ static int proofDepth;
|
|||
static int max_encryption_level;
|
||||
static int num_regular_runs;
|
||||
static int num_intruder_runs;
|
||||
static FILE *attack_stream;
|
||||
|
||||
struct goalstruct
|
||||
{
|
||||
|
|
@ -740,6 +741,13 @@ proof_suppose_binding (Binding b)
|
|||
}
|
||||
}
|
||||
|
||||
//! Create a new temporary file and return the pointer.
|
||||
FILE *
|
||||
scyther_tempfile (void)
|
||||
{
|
||||
return tmpfile ();
|
||||
}
|
||||
|
||||
//------------------------------------------------------------------------
|
||||
// Sub
|
||||
//------------------------------------------------------------------------
|
||||
|
|
@ -3206,7 +3214,8 @@ prune_bounds ()
|
|||
if (switches.maxIntruderActions < INT_MAX || !(switches.intruder))
|
||||
{
|
||||
// Only check if actually used
|
||||
if (!(switches.intruder) || countIntruderActions () > switches.maxIntruderActions)
|
||||
if (!(switches.intruder)
|
||||
|| countIntruderActions () > switches.maxIntruderActions)
|
||||
{
|
||||
if (switches.output == PROOF)
|
||||
{
|
||||
|
|
@ -3474,12 +3483,62 @@ makeTraceClass (const System sys, Termlist varlist)
|
|||
termlistDelete (varlist);
|
||||
}
|
||||
|
||||
//! Start attack output
|
||||
void
|
||||
attackOutputStart (void)
|
||||
{
|
||||
if (switches.prune == 2)
|
||||
{
|
||||
FILE *fd;
|
||||
|
||||
// Close old file (if any)
|
||||
if (attack_stream != NULL)
|
||||
{
|
||||
fclose (attack_stream); // this automatically discards the old temporary file
|
||||
}
|
||||
// Create new file
|
||||
fd = scyther_tempfile ();
|
||||
attack_stream = fd;
|
||||
globalStream = (char *) attack_stream;
|
||||
}
|
||||
}
|
||||
|
||||
//! Stop attack output
|
||||
void
|
||||
attackOutputStop (void)
|
||||
{
|
||||
// Nothing to do, just leave the opened tmpfile
|
||||
}
|
||||
|
||||
//! Copy one (finite) stream from beginning to end to another
|
||||
/**
|
||||
* Ugly first implementation, something to improve later (although it is not
|
||||
* crucial code in any way)
|
||||
*/
|
||||
void
|
||||
fcopy (FILE * fromstream, FILE * tostream)
|
||||
{
|
||||
int c;
|
||||
|
||||
// 'Just to be sure'
|
||||
fflush (fromstream);
|
||||
fseek (fromstream, 0, SEEK_SET);
|
||||
|
||||
// Urgh, using the assignment in the loop condition, brrr. Fugly.
|
||||
// Discourage.
|
||||
while ((c = fgetc (fromstream)) != EOF)
|
||||
{
|
||||
fputc (c, tostream);
|
||||
}
|
||||
}
|
||||
|
||||
//! Output an attack in the desired way
|
||||
void
|
||||
arachneOutputAttack ()
|
||||
{
|
||||
Termlist varlist;
|
||||
|
||||
// Make concrete
|
||||
if (switches.concrete)
|
||||
{
|
||||
varlist = makeTraceConcrete (sys);
|
||||
|
|
@ -3489,6 +3548,10 @@ arachneOutputAttack ()
|
|||
varlist = NULL;
|
||||
}
|
||||
|
||||
// Wrapper for the real output
|
||||
attackOutputStart ();
|
||||
|
||||
// Generate the output, already!
|
||||
if (switches.xml)
|
||||
{
|
||||
xmlOutSemitrace (sys);
|
||||
|
|
@ -3505,6 +3568,10 @@ arachneOutputAttack ()
|
|||
}
|
||||
}
|
||||
|
||||
// End wrapper
|
||||
attackOutputStop ();
|
||||
|
||||
// Undo concretization
|
||||
makeTraceClass (sys, varlist);
|
||||
}
|
||||
|
||||
|
|
@ -3652,6 +3719,50 @@ iterate ()
|
|||
return flag;
|
||||
}
|
||||
|
||||
//! Just before starting output of an attack.
|
||||
//
|
||||
//! A wrapper for the case in which we need to buffer attacks.
|
||||
int
|
||||
iterate_buffer_attacks (void)
|
||||
{
|
||||
if (switches.prune != 2)
|
||||
{
|
||||
return iterate ();
|
||||
}
|
||||
else
|
||||
{
|
||||
// We are pruning attacks, so they should go into a temporary file.
|
||||
/*
|
||||
* Set up the temporary file pointer
|
||||
*/
|
||||
char *buffer;
|
||||
int result;
|
||||
|
||||
// Push the old situation onto the stack
|
||||
buffer = globalStream;
|
||||
|
||||
// Start stuff
|
||||
attack_stream = NULL;
|
||||
attackOutputStart ();
|
||||
|
||||
// Finally, proceed with iteration procedure
|
||||
result = iterate ();
|
||||
|
||||
/* Now, if it has been set, we need to copy the output to the normal streams.
|
||||
*/
|
||||
fcopy (attack_stream, (FILE *) buffer);
|
||||
|
||||
// Close
|
||||
fclose (attack_stream);
|
||||
attack_stream = NULL;
|
||||
|
||||
// Restore
|
||||
globalStream = buffer;
|
||||
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
//! Main code for Arachne
|
||||
/**
|
||||
* For this test, we manually set up some stuff.
|
||||
|
|
@ -3770,14 +3881,14 @@ arachne ()
|
|||
add_claim_specifics (cl,
|
||||
roledef_shift (sys->runs[run].start,
|
||||
cl->ev));
|
||||
|
||||
#ifdef DEBUG
|
||||
if (DEBUGL (5))
|
||||
{
|
||||
printSemiState ();
|
||||
}
|
||||
#endif
|
||||
// Iterate
|
||||
iterate ();
|
||||
iterate_buffer_attacks ();
|
||||
|
||||
//! Destroy
|
||||
while (sys->bindings != NULL)
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ switchesInit (int argc, char **argv)
|
|||
switches.tupling = 0;
|
||||
|
||||
// Pruning and Bounding
|
||||
switches.prune = 2; // default pruning method
|
||||
switches.prune = 2; // default pruning method (just output a single one)
|
||||
switches.maxproofdepth = INT_MAX;
|
||||
switches.maxtracelength = INT_MAX;
|
||||
switches.runs = 5; // default is 5 for usability, but -r 0 or --maxruns=0 will set it back to INT_MAX
|
||||
|
|
@ -444,7 +444,7 @@ switcher (const int process, int index)
|
|||
if (!process)
|
||||
{
|
||||
/* not very important
|
||||
helptext ("-p,--prune=<int>", "pruning method when an attack is found [0]");
|
||||
helptext ("-p,--prune=<int>", "pruning method when an attack is found [2]");
|
||||
*/
|
||||
}
|
||||
else
|
||||
|
|
|
|||
12
src/symbol.c
12
src/symbol.c
|
|
@ -18,6 +18,7 @@
|
|||
/* accessible for externals */
|
||||
|
||||
int globalError; //!< If >0, stdout output goes to stderr (for e.g. terms)
|
||||
char *globalStream; //!< Defaults to stdout
|
||||
|
||||
/* external declarations */
|
||||
|
||||
|
|
@ -45,6 +46,7 @@ symbolsInit (void)
|
|||
symb_list = NULL;
|
||||
symb_alloc = NULL;
|
||||
globalError = 0;
|
||||
globalStream = stdout;
|
||||
}
|
||||
|
||||
//! Close symbols code.
|
||||
|
|
@ -255,7 +257,13 @@ symbol_fix_keylevels (void)
|
|||
|
||||
//! Print out according to globalError
|
||||
/**
|
||||
* Input is comparable to printf, only depends on globalError. This should be used by any function trying to do output.
|
||||
* Input is comparable to printf, only depends on globalError. This should be
|
||||
* used by any function trying to do output.
|
||||
*
|
||||
* Furthermore, if globalError == 0, it can still be overriden by
|
||||
* globalStream, which can be another stream pointer. If it is null, stdout
|
||||
* is assumed.
|
||||
*
|
||||
*\sa globalError
|
||||
*/
|
||||
void
|
||||
|
|
@ -265,7 +273,7 @@ eprintf (char *fmt, ...)
|
|||
|
||||
va_start (args, fmt);
|
||||
if (globalError == 0)
|
||||
vfprintf (stdout, fmt, args);
|
||||
vfprintf ((FILE *) globalStream, fmt, args);
|
||||
else
|
||||
vfprintf (stderr, fmt, args);
|
||||
va_end (args);
|
||||
|
|
|
|||
|
|
@ -48,5 +48,6 @@ void symbol_fix_keylevels (void);
|
|||
void eprintf (char *fmt, ...);
|
||||
|
||||
extern int globalError;
|
||||
extern char *globalStream;
|
||||
|
||||
#endif
|
||||
|
|
|
|||
114
src/xmlout.c
114
src/xmlout.c
|
|
@ -43,7 +43,7 @@ static int show_substitution_path; // is only set to true for variable printing,
|
|||
void
|
||||
xmlOutInit (void)
|
||||
{
|
||||
printf ("<scyther>\n");
|
||||
eprintf ("<scyther>\n");
|
||||
xmlindent = 1;
|
||||
only_claim_label = NULL;
|
||||
show_substitution_path = false;
|
||||
|
|
@ -53,7 +53,7 @@ xmlOutInit (void)
|
|||
void
|
||||
xmlOutDone (void)
|
||||
{
|
||||
printf ("</scyther>\n");
|
||||
eprintf ("</scyther>\n");
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
@ -69,14 +69,14 @@ xmlIndentPrint ()
|
|||
i = xmlindent;
|
||||
while (i > 0)
|
||||
{
|
||||
printf (" ");
|
||||
eprintf (" ");
|
||||
i--;
|
||||
}
|
||||
}
|
||||
|
||||
//! XML print
|
||||
/**
|
||||
* Input is comparable to printf, but indents (according to xmlindent) and adds
|
||||
* Input is comparable to eprintf, but indents (according to xmlindent) and adds
|
||||
* a newline.
|
||||
*/
|
||||
void
|
||||
|
|
@ -86,9 +86,9 @@ xmlPrint (char *fmt, ...)
|
|||
|
||||
xmlIndentPrint ();
|
||||
va_start (args, fmt);
|
||||
vfprintf (stdout, fmt, args);
|
||||
eprintf (fmt, args);
|
||||
va_end (args);
|
||||
printf ("\n");
|
||||
eprintf ("\n");
|
||||
}
|
||||
|
||||
//! Print a simple integer value element
|
||||
|
|
@ -126,12 +126,12 @@ xmlTermPrintInner (Term term)
|
|||
{
|
||||
Term substbuffer;
|
||||
|
||||
printf ("<var name=\"");
|
||||
eprintf ("<var name=\"");
|
||||
if (term->subst == NULL)
|
||||
{
|
||||
// Free variable
|
||||
termPrint (term); // Must be a normal termPrint
|
||||
printf ("\" free=\"true\" />");
|
||||
eprintf ("\" free=\"true\" />");
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -140,17 +140,17 @@ xmlTermPrintInner (Term term)
|
|||
term->subst = NULL;
|
||||
termPrint (term); // Must be a normal termPrint
|
||||
term->subst = substbuffer;
|
||||
printf ("\">");
|
||||
eprintf ("\">");
|
||||
xmlTermPrintInner (term->subst);
|
||||
printf ("</var>");
|
||||
eprintf ("</var>");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// Constant
|
||||
printf ("<const>");
|
||||
eprintf ("<const>");
|
||||
termPrint (term); // Must be a normal termPrint
|
||||
printf ("</const>");
|
||||
eprintf ("</const>");
|
||||
}
|
||||
}
|
||||
else
|
||||
|
|
@ -162,29 +162,29 @@ xmlTermPrintInner (Term term)
|
|||
&& inTermlist (TermKey (term)->stype, TERM_Function))
|
||||
{
|
||||
/* function application */
|
||||
printf ("<apply><function>");
|
||||
eprintf ("<apply><function>");
|
||||
xmlTermPrintInner (TermKey (term));
|
||||
printf ("</function><arg>");
|
||||
eprintf ("</function><arg>");
|
||||
xmlTermPrintInner (TermOp (term));
|
||||
printf ("</arg></apply>");
|
||||
eprintf ("</arg></apply>");
|
||||
}
|
||||
else
|
||||
{
|
||||
printf ("<encrypt><op>");
|
||||
eprintf ("<encrypt><op>");
|
||||
xmlTermPrintInner (TermOp (term));
|
||||
printf ("</op><key>");
|
||||
eprintf ("</op><key>");
|
||||
xmlTermPrintInner (TermKey (term));
|
||||
printf ("</key></encrypt>");
|
||||
eprintf ("</key></encrypt>");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// Assume tuple
|
||||
printf ("<tuple><op1>");
|
||||
eprintf ("<tuple><op1>");
|
||||
xmlTermPrintInner (TermOp1 (term));
|
||||
printf ("</op1><op2>");
|
||||
eprintf ("</op1><op2>");
|
||||
xmlTermPrintInner (TermOp2 (term));
|
||||
printf ("</op2></tuple>");
|
||||
eprintf ("</op2></tuple>");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -199,9 +199,9 @@ xmlTermPrintInner (Term term)
|
|||
void
|
||||
xmlTermPrint (const Term term)
|
||||
{
|
||||
// printf ("<term>");
|
||||
// eprintf ("<term>");
|
||||
xmlTermPrintInner (term);
|
||||
// printf ("</term>");
|
||||
// eprintf ("</term>");
|
||||
}
|
||||
|
||||
//! Print a termlist in XML form
|
||||
|
|
@ -214,7 +214,7 @@ xmlTermlistPrint (Termlist tl)
|
|||
{
|
||||
xmlIndentPrint ();
|
||||
xmlTermPrint (tl->term);
|
||||
printf ("\n");
|
||||
eprintf ("\n");
|
||||
tl = tl->next;
|
||||
}
|
||||
xmlindent--;
|
||||
|
|
@ -232,11 +232,11 @@ xmlOutTerm (const char *tag, const Term term)
|
|||
{
|
||||
xmlIndentPrint ();
|
||||
if (tag != NULL)
|
||||
printf ("<%s>", tag);
|
||||
eprintf ("<%s>", tag);
|
||||
xmlTermPrint (term);
|
||||
if (tag != NULL)
|
||||
printf ("</%s>", tag);
|
||||
printf ("\n");
|
||||
eprintf ("</%s>", tag);
|
||||
eprintf ("\n");
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -246,9 +246,9 @@ xmlAttrTerm (const char *tag, const Term term)
|
|||
{
|
||||
if (term != NULL)
|
||||
{
|
||||
printf (" %s=\"", tag);
|
||||
eprintf (" %s=\"", tag);
|
||||
xmlTermPrint (term);
|
||||
printf ("\"");
|
||||
eprintf ("\"");
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -276,9 +276,9 @@ void
|
|||
xmlRoleTermPrint (const Term t)
|
||||
{
|
||||
xmlIndentPrint ();
|
||||
printf ("<rolename>");
|
||||
eprintf ("<rolename>");
|
||||
roleTermPrint (t);
|
||||
printf ("</rolename>\n");
|
||||
eprintf ("</rolename>\n");
|
||||
}
|
||||
|
||||
//! Show a single variable instantiation, depth one
|
||||
|
|
@ -307,7 +307,7 @@ xmlVariableDepthOne (const Term variable)
|
|||
// Print the actual term
|
||||
xmlIndentPrint ();
|
||||
xmlTermPrint (variable);
|
||||
printf ("\n");
|
||||
eprintf ("\n");
|
||||
|
||||
if (nextsubst != NULL)
|
||||
{
|
||||
|
|
@ -333,7 +333,7 @@ xmlTermType (const Term t)
|
|||
xmlindent++;
|
||||
xmlIndentPrint ();
|
||||
xmlTermPrint (t);
|
||||
printf ("\n");
|
||||
eprintf ("\n");
|
||||
xmlindent--;
|
||||
xmlPrint ("</term>");
|
||||
|
||||
|
|
@ -357,16 +357,16 @@ xmlVariable (const System sys, const Term variable, const int run)
|
|||
if (realTermVariable (variable))
|
||||
{
|
||||
xmlIndentPrint ();
|
||||
printf ("<variable typeflaw=\"");
|
||||
eprintf ("<variable typeflaw=\"");
|
||||
if (!checkTypeTerm (0, variable))
|
||||
{
|
||||
printf ("true");
|
||||
eprintf ("true");
|
||||
}
|
||||
else
|
||||
{
|
||||
printf ("false");
|
||||
eprintf ("false");
|
||||
}
|
||||
printf ("\" run=\"%i\">\n", run);
|
||||
eprintf ("\" run=\"%i\">\n", run);
|
||||
xmlindent++;
|
||||
|
||||
xmlPrint ("<name>");
|
||||
|
|
@ -531,29 +531,29 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
|
|||
|
||||
xmlIndentPrint ();
|
||||
|
||||
printf ("<event type=\"");
|
||||
eprintf ("<event type=\"");
|
||||
switch (rd->type)
|
||||
{
|
||||
/* Read or send types are fairly similar.
|
||||
* Currently, choose events are not distinguished yet. TODO
|
||||
*/
|
||||
case READ:
|
||||
printf ("read");
|
||||
eprintf ("read");
|
||||
break;
|
||||
case SEND:
|
||||
printf ("send");
|
||||
eprintf ("send");
|
||||
break;
|
||||
case CLAIM:
|
||||
printf ("claim");
|
||||
eprintf ("claim");
|
||||
break;
|
||||
default:
|
||||
printf ("unknown code=\"%i\"", rd->type);
|
||||
eprintf ("unknown code=\"%i\"", rd->type);
|
||||
break;
|
||||
}
|
||||
|
||||
printf ("\"");
|
||||
printf (" index=\"%i\"", index);
|
||||
printf (">\n");
|
||||
eprintf ("\"");
|
||||
eprintf (" index=\"%i\"", index);
|
||||
eprintf (">\n");
|
||||
xmlindent++;
|
||||
xmlOutTerm ("label", rd->label);
|
||||
if (rd->type != CLAIM)
|
||||
|
|
@ -596,7 +596,7 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
|
|||
xmlindent++;
|
||||
xmlIndentPrint ();
|
||||
xmlTermPrint (b->term);
|
||||
printf ("\n");
|
||||
eprintf ("\n");
|
||||
xmlindent--;
|
||||
|
||||
xmlPrint ("</choose>");
|
||||
|
|
@ -612,10 +612,10 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
|
|||
else
|
||||
xmlPrint ("<unbound />");
|
||||
if (b->blocked)
|
||||
printf ("<blocked />");
|
||||
eprintf ("<blocked />");
|
||||
xmlIndentPrint ();
|
||||
xmlTermPrint (b->term);
|
||||
printf ("\n");
|
||||
eprintf ("\n");
|
||||
xmlindent--;
|
||||
|
||||
xmlPrint ("</follows>");
|
||||
|
|
@ -770,22 +770,22 @@ xmlRunInfo (const System sys, const int run)
|
|||
|
||||
xmlOutInteger ("runid", run);
|
||||
xmlIndentPrint ();
|
||||
printf ("<protocol");
|
||||
eprintf ("<protocol");
|
||||
if (sys->runs[run].protocol == INTRUDER)
|
||||
{
|
||||
printf (" intruder=\"true\"");
|
||||
eprintf (" intruder=\"true\"");
|
||||
}
|
||||
else
|
||||
{
|
||||
// Non-intruder run, check whether communicates with untrusted agents
|
||||
if (!isRunTrusted (sys, run))
|
||||
{
|
||||
printf (" untrustedrun=\"true\"");
|
||||
eprintf (" untrustedrun=\"true\"");
|
||||
}
|
||||
}
|
||||
printf (">");
|
||||
eprintf (">");
|
||||
xmlTermPrint (sys->runs[run].protocol->nameterm);
|
||||
printf ("</protocol>\n");
|
||||
eprintf ("</protocol>\n");
|
||||
r = sys->runs[run].role;
|
||||
|
||||
/* undo substitution temporarily to retrieve role name */
|
||||
|
|
@ -925,15 +925,15 @@ xmlOutSemitrace (const System sys)
|
|||
Term buffer_only_claim_label;
|
||||
|
||||
xmlIndentPrint ();
|
||||
printf ("<attack");
|
||||
eprintf ("<attack");
|
||||
/* add trace length attribute */
|
||||
/* Note that this is the length of the attack leading up to the broken
|
||||
* claim, thus without any run extensions (--extend-nonreads).
|
||||
*/
|
||||
printf (" tracelength=\"%i\"", get_semitrace_length ());
|
||||
eprintf (" tracelength=\"%i\"", get_semitrace_length ());
|
||||
/* add attack id attribute (within this scyther call) */
|
||||
printf (" id=\"%i\"", sys->attackid);
|
||||
printf (">\n");
|
||||
eprintf (" id=\"%i\"", sys->attackid);
|
||||
eprintf (">\n");
|
||||
xmlindent++;
|
||||
|
||||
/* mention the broken claim */
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user