diff --git a/src/arachne.c b/src/arachne.c index 085f28e..25e7151 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -437,7 +437,7 @@ determine_unification_run (Termlist tl) //! Determine trace length int -get_trace_length () +get_semitrace_length () { int run; int length; @@ -608,16 +608,16 @@ int iterate_role_sends (int (*func) ()) { int send_wrapper (Protocol p, Role r, Roledef rd, int i) - { - if (rd->type == SEND) - { - return func (p,r,rd,i); - } - else - { - return 1; - } - } + { + if (rd->type == SEND) + { + return func (p, r, rd, i); + } + else + { + return 1; + } + } return iterate_role_events (send_wrapper); } @@ -1571,7 +1571,7 @@ printSemiState () indentPrint (); eprintf ("!!\n"); indentPrint (); - eprintf ("!! Trace length: %i\n", get_trace_length ()); + eprintf ("!! Trace length: %i\n", get_semitrace_length ()); open = 0; for (run = 0; run < sys->maxruns; run++) { @@ -1718,7 +1718,8 @@ isOpenNonceVar (Term t) //! Count unique open variables in term /** */ -int count_open_variables (const Term t) +int +count_open_variables (const Term t) { Termlist tl; int n; @@ -1758,7 +1759,7 @@ term_noncevariables_level (const Term t) } else { - return 1 - (onv/enough); + return 1 - (onv / enough); } } @@ -1880,13 +1881,13 @@ select_goal () } void erode (const int w, const float fl) - { - if (smode & 1) - { - adapt (w,fl); - } - smode = smode / 2; - } + { + if (smode & 1) + { + adapt (w, fl); + } + smode = smode / 2; + } // buf_constrain is the addition of the factors before division by weight buf_constrain = 0; @@ -1900,15 +1901,15 @@ select_goal () // Determine buf_constrain levels // Bit 0: 1 constrain level - erode (1, term_constrain_level (b->term)); + erode (1, term_constrain_level (b->term)); // Bit 1: 2 key level (inverted) - erode (1, 0.5 * (1 - b->level)); + erode (1, 0.5 * (1 - b->level)); // Bit 2: 4 consequence level - erode (1, termBindConsequences (b->term)); + erode (1, termBindConsequences (b->term)); // Bit 3: 8 single variables first - erode (1, 1 - isTermVariable (b->term)); + erode (1, 1 - isTermVariable (b->term)); // Bit 4: 16 nonce variables level (Cf. what I think is in Athena) - erode (1, term_noncevariables_level (b->term)); + erode (1, term_noncevariables_level (b->term)); // Define legal range if (smode > 0) error ("--goal-select mode %i is illegal", mode); @@ -2725,7 +2726,7 @@ prune_bounds () } // Limit on exceeding any attack length - if (sys->prune == 2 && get_trace_length () >= attack_length) + if (sys->prune == 2 && get_semitrace_length () >= attack_length) { if (sys->output == PROOF) { @@ -2835,17 +2836,24 @@ property_check () count_false (); if (sys->output == ATTACK) { - if (sys->latex == 1) + if (sys->switchXMLoutput) { - latexSemiState (); + xmlOutSemitrace (sys); } else { - dotSemiState (); + if (sys->latex == 1) + { + latexSemiState (); + } + else + { + dotSemiState (); + } } } // Store attack length if shorter - attack_this = get_trace_length (); + attack_this = get_semitrace_length (); if (attack_this < attack_length) { // Shortest attack @@ -2989,10 +2997,10 @@ arachne () int determine_encrypt_max (Protocol p, Role r, Roledef rd, int index) { int tlevel; - + tlevel = term_encryption_level (rd->message); #ifdef DEBUG - if (DEBUGL(3)) + if (DEBUGL (3)) { eprintf ("Encryption level %i found for term ", tlevel); termPrint (rd->message); diff --git a/src/arachne.h b/src/arachne.h index 1d9a403..a00791c 100644 --- a/src/arachne.h +++ b/src/arachne.h @@ -6,5 +6,6 @@ void arachneInit (const System sys); void arachneDone (); int arachne (); +int get_semitrace_length (); #endif diff --git a/src/switches.c b/src/switches.c index 6b8f224..1f56337 100644 --- a/src/switches.c +++ b/src/switches.c @@ -114,7 +114,7 @@ switcher (const int process, const System sys, int index) // It's the right thing if (optlength + 3 < this_arg_length) { - arg_pointer = this_arg + 2 + optlength + 1; + arg_pointer = this_arg + 2 + optlength + 1; } else { @@ -177,7 +177,7 @@ switcher (const int process, const System sys, int index) } #endif this_arg = argv[index]; - this_arg_length = strlen(this_arg); + this_arg_length = strlen (this_arg); } else { @@ -210,6 +210,19 @@ switcher (const int process, const System sys, int index) } } + if (detect ('x', "xml-output", 0)) + { + if (!process) + { + helptext ("-x,--xml-output", "show attack output in XML format"); + } + else + { + sys->switchXMLoutput = 1; + return index; + } + } + if (detect ('m', "match", 1)) { if (!process) @@ -517,9 +530,10 @@ switcher (const int process, const System sys, int index) { fprintf (stderr, "Unknown switch '%s'.\n", this_arg); } - else + else { - fprintf (stderr, "Could not open input file '%s'.\n", this_arg); + fprintf (stderr, "Could not open input file '%s'.\n", + this_arg); } exit (1); } diff --git a/src/system.c b/src/system.c index ec05230..ad0a6b8 100644 --- a/src/system.c +++ b/src/system.c @@ -75,8 +75,9 @@ systemInit () sys->switchReduceClaims = 1; // default remove claims from duplicate instance choosers sys->switchClaims = 0; // default don't report on claims sys->switchClaimToCheck = NULL; // default check all claims + sys->switchXMLoutput = 0; // default no xml output sys->switchGoalSelectMethod = 3; // default goal selection method - sys->traverse = 12; // default traversal method + sys->traverse = 12; // default traversal method sys->switch_maxproofdepth = INT_MAX; sys->switch_maxtracelength = INT_MAX; @@ -262,7 +263,8 @@ ensureValidRun (const System sys, int run) /* update size parameter */ oldsize = sys->maxruns; sys->maxruns = run + 1; - sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); + sys->runs = + (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); /* create runs, set the new pointer(s) to NULL */ for (i = oldsize; i < sys->maxruns; i++) @@ -369,7 +371,7 @@ agentOfRunRole (const System sys, const int run, const Term role) // Non-arachne Termlist roles; Termlist agents; - + roles = sys->runs[run].protocol->rolenames; agents = sys->runs[run].agents; @@ -408,7 +410,7 @@ agentOfRunRole (const System sys, const int run, const Term role) Term agent; agent = agents->term; - if (TermSymb(role) == TermSymb(agent)) + if (TermSymb (role) == TermSymb (agent)) { return agent; } @@ -671,15 +673,15 @@ roleInstanceArachne (const System sys, const Protocol protocol, Run runs; Roledef rd; Termlist scanfrom, scanto; - Termlist fromlist = NULL; // deleted at the end - Termlist tolist = NULL; // -> .locals - Termlist artefacts = NULL; // -> .artefacts - Term extterm = NULL; // construction thing (will go to artefacts) + Termlist fromlist = NULL; // deleted at the end + Termlist tolist = NULL; // -> .locals + Termlist artefacts = NULL; // -> .artefacts + Term extterm = NULL; // construction thing (will go to artefacts) /* claim runid, allocate space */ rid = sys->maxruns; - ensureValidRun (sys, rid); // creates a new block - runs = sys->runs; // simple structure pointer transfer (shortcut) + ensureValidRun (sys, rid); // creates a new block + runs = sys->runs; // simple structure pointer transfer (shortcut) /* duplicate roledef in buffer rd */ /* Notice that it is not stored (yet) in the run structure, @@ -712,7 +714,7 @@ roleInstanceArachne (const System sys, const Protocol protocol, * of it again. */ oldt = scanfrom->term; - newt = deVar(oldt); + newt = deVar (oldt); if (realTermVariable (newt)) { /* This is a variable of the role, that is not instantiated yet. @@ -735,7 +737,7 @@ roleInstanceArachne (const System sys, const Protocol protocol, if (isTermVariable (newt)) { // It is a protocol role name - + // Flag this newt->roleVar = 1; newt->stype = termlistAddNew (newt->stype, TERM_Agent); @@ -1035,31 +1037,31 @@ roleInstanceDestroy (const System sys) } substlist = substlist->next; } - termlistDelete(myrun.substitutions); + termlistDelete (myrun.substitutions); // sys->variables might contain locals from the run: remove them - { - Termlist tl; + { + Termlist tl; - tl = sys->variables; - while (tl != NULL) - { - Term t; + tl = sys->variables; + while (tl != NULL) + { + Term t; - t = tl->term; - if (realTermLeaf(t) && TermRunid(t) == runid) - { - // remove from list; return pointer to head - sys->variables = termlistDelTerm (tl); - tl = sys->variables; - } - else - { - // proceed - tl = tl->next; - } - } - } + t = tl->term; + if (realTermLeaf (t) && TermRunid (t) == runid) + { + // remove from list; return pointer to head + sys->variables = termlistDelTerm (tl); + tl = sys->variables; + } + else + { + // proceed + tl = tl->next; + } + } + } // remove lists termlistDelete (myrun.artefacts); @@ -1069,7 +1071,8 @@ roleInstanceDestroy (const System sys) // Destroy run struct allocation in array using realloc // Reduce run count sys->maxruns = sys->maxruns - 1; - sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); + sys->runs = + (Run) memRealloc (sys->runs, sizeof (struct run) * (sys->maxruns)); } } diff --git a/src/system.h b/src/system.h index 8122da2..2e07857 100644 --- a/src/system.h +++ b/src/system.h @@ -143,6 +143,7 @@ struct system int switchClaims; //!< Enable clails report int switchGoalSelectMethod; //!< Goal selection method for Arachne engine Term switchClaimToCheck; //!< Which claim should be checked? + int switchXMLoutput; //!< xml output //! Latex output switch. /** diff --git a/src/xmlout.c b/src/xmlout.c new file mode 100644 index 0000000..b46a189 --- /dev/null +++ b/src/xmlout.c @@ -0,0 +1,336 @@ +/* + * xmlout.c + * + * XML output for Scyther + * + * Module to output detailed Scyther information in XML format, for easier + * interaction with external programs. Originally developed for attack output + * details. + */ + +#include +#include +#include + +#include "term.h" +#include "termlist.h" +#include "system.h" +#include "binding.h" +#include "arachne.h" // for get_semitrace_length + +#include "xmlout.h" + +/* + * Global/static stuff. + */ +static int xmlindent; // indent level for xml elements in output + +/* + * Default external interface: init/done + */ + +//! Init this module +void +xmlOutInit (void) +{ + xmlindent = 0; +} + +//! Close up +void +xmlOutDone (void) +{ +} + +/* + * Local code, needed for any further real code. + */ + +//! Indent code +void +xmlIndentPrint () +{ + int i; + + i = xmlindent; + while (i > 0) + { + printf (" "); + i--; + } +} + +//! XML print +/** + * Input is comparable to printf, but indents (according to xmlindent) and adds + * a newline. + */ +void +xmlPrint (char *fmt, ...) +{ + va_list args; + + xmlIndentPrint (); + va_start (args, fmt); + vfprintf (stdout, fmt, args); + va_end (args); + printf ("\n"); +} + +//! Print a simple integer value element +void +xmlOutInteger (const char *tag, const int value) +{ + xmlPrint ("<%s>%i", tag, value, tag); +} + +//! Print a term for an element +void +xmlOutTerm (const char *tag, const Term term) +{ + if (term != NULL) + { + xmlIndentPrint (); + printf ("<%s>", tag); + termPrint (term); + printf ("\n", tag); + } +} + +//! Attribute term +void +xmlAttrTerm (const char *tag, const Term term) +{ + if (term != NULL) + { + printf (" %s=\"", tag); + termPrint (term); + printf ("\""); + } +} + +//! Global system info +/** + * To be used by concrete trace as well as semitrace output + */ +void +xmlOutSysInfo (const System sys) +{ + xmlPrint (""); + xmlindent++; + + { + Protocol p; + + p = sys->protocols; + while (p != NULL) + { + xmlOutTerm ("protocol", p->nameterm); + p = p->next; + } + } + + xmlOutInteger ("match", sys->match); + + xmlindent--; + xmlPrint (""); +} + +//! Static information about a run +/** + * TODO: Does not output any sigma info yet (role->agent mappings), which is very important. + */ +void +xmlRunInfo (const System sys, const int run) +{ + Role r; + Term oldagent; + + xmlOutInteger ("runid", run); + xmlOutTerm ("protocol", sys->runs[run].protocol->nameterm); + r = sys->runs[run].role; + + /* undo substitution temporarily to retrieve role name */ + /* Note that this is fairly tailored towards the Arachne method, TODO: make + * more generic. */ + oldagent = r->nameterm->subst; + r->nameterm->subst = NULL; + xmlOutTerm ("role", r->nameterm); + /* reinstate substitution */ + r->nameterm->subst = oldagent; + if (oldagent != NULL) + { + xmlOutTerm ("agent", r->nameterm); + } +} + +//! Show a single event from a run +/** + * run and index will only be output if they are nonnegative. + */ +void +xmlOutEvent (const System sys, Roledef rd, const int run, const int index) +{ + xmlIndentPrint (); + + printf ("<"); + switch (rd->type) + { + /* Read or send types are fairly similar. + * Currently, choose events are not distinguished yet. TODO + */ + case READ: + printf ("read"); + break; + case SEND: + printf ("send"); + break; + case CLAIM: + printf ("claim"); + break; + default: + printf ("unknown code=\"%i\"", rd->type); + break; + } + + xmlAttrTerm ("label", rd->label); + if (rd->type != CLAIM) + { + /* read or send */ + xmlAttrTerm ("from", rd->from); + xmlAttrTerm ("to", rd->to); + xmlAttrTerm ("message", rd->message); + } + else + { + /* claim */ + xmlAttrTerm ("role", rd->from); + xmlAttrTerm ("type", rd->to); + xmlAttrTerm ("argument", rd->message); + } + + if (run >= 0) + { + printf (" run=\"%i\"", run); + } + if (index >= 0) + { + printf (" index=\"%i\"", index); + } + printf (" />\n"); +} + +//! Display runs +void +xmlOutRuns (const System sys) +{ + int run; + + for (run = 0; run < sys->maxruns; run++) + { + xmlPrint (""); + xmlindent++; + + xmlRunInfo (sys, run); + + xmlPrint (""); + xmlindent++; + { + Roledef rd; + int index; + + index = 0; + rd = sys->runs[run].start; + while (rd != NULL) + { + xmlOutEvent (sys, rd, -1, index); + index++; + rd = rd->next; + } + } + xmlindent--; + xmlPrint (""); + xmlindent--; + xmlPrint (""); + } +} + + +//! Output list of bindings +void +xmlOutBindings (const System sys) +{ + int xmlBindingState (void *dt) + { + Binding b; + void xmlRunIndex (char *desc, const int run, const int index) + { + xmlPrint ("<%s run=\"%i\" index=\"%i\" />", desc, run, index); + } + + b = (Binding) dt; + xmlIndentPrint (); + printf ("term); + printf ("\" />\n"); + xmlindent++; + if (b->done) + xmlRunIndex ("from", b->run_from, b->ev_from); + else + xmlPrint (""); + xmlRunIndex ("to", b->run_to, b->ev_to); + if (b->blocked) + printf (""); + xmlindent--; + xmlPrint (""); + return 1; + } + + xmlPrint (""); + xmlindent++; + if (sys->bindings != NULL) + { + list_iterate (sys->bindings, xmlBindingState); + } + xmlindent--; + xmlPrint (""); +} + +/* + * ----------------------------------------------------------------------------------- + * Publicly available functions + */ + +//! Output for a concrete trace (from modelchecker) +void +xmlOutTrace (const System sys) +{ +} + +//! Output for a semitrace (from arachne method) +/** + * Note: Uses get_trace_length(), which is defined for the arachne method only. + * + * TODO does not show violated claim yet, this must now be guessed by the + * reader. + */ +void +xmlOutSemitrace (const System sys) +{ + xmlIndentPrint (); + printf ("\n"); + xmlindent++; + /* any global information about the system */ + xmlOutSysInfo (sys); + xmlPrint (""); + xmlindent++; + xmlOutRuns (sys); + xmlOutBindings (sys); + xmlindent--; + xmlPrint (""); + xmlindent--; + xmlPrint (""); +} diff --git a/src/xmlout.h b/src/xmlout.h new file mode 100644 index 0000000..3595237 --- /dev/null +++ b/src/xmlout.h @@ -0,0 +1,12 @@ +#ifndef XMLOUT +#define XMLOUT + +#include "system.h" + +void xmlOutInit (void); +void xmlOutDone (void); + +void xmlOutSemitrace (const System sys); +void xmlOutTrace (const System sys); + +#endif