- --max-attacks=AnyGijsNumber.
This commit is contained in:
parent
998e4852ba
commit
1ee77472a0
@ -3094,6 +3094,10 @@ prune_bounds ()
|
||||
return 1;
|
||||
}
|
||||
|
||||
// Limit on attack count
|
||||
if (enoughAttacks (sys))
|
||||
return 1;
|
||||
|
||||
// No pruning because of bounds
|
||||
return 0;
|
||||
}
|
||||
@ -3192,6 +3196,10 @@ property_check ()
|
||||
|
||||
flag = 1;
|
||||
|
||||
/* Do we need any? */
|
||||
if (enoughAttacks (sys))
|
||||
return flag;
|
||||
|
||||
/**
|
||||
* By the way the claim is handled, this automatically means a flaw.
|
||||
*/
|
||||
|
@ -177,6 +177,10 @@ executeStep (const System sys, const int run)
|
||||
if (!sys->explore)
|
||||
return 0;
|
||||
|
||||
/* prune (exit) if enough attacks found */
|
||||
if (enoughAttacks (sys))
|
||||
return 0;
|
||||
|
||||
/* we want to explore it, but are we allowed by pruning? */
|
||||
if (sys->step >= sys->maxtracelength)
|
||||
{
|
||||
@ -260,7 +264,7 @@ removeDangling (Roledef rd, const int killclaims)
|
||||
Roledef
|
||||
removeIrrelevant (const System sys, const int run, Roledef rd)
|
||||
{
|
||||
if (!isRunTrusted (sys,run))
|
||||
if (!isRunTrusted (sys, run))
|
||||
{
|
||||
// untrusted, so also remove claims
|
||||
return removeDangling (rd, 1);
|
||||
@ -384,7 +388,7 @@ explorify (const System sys, const int run)
|
||||
while (rid < sys->maxruns)
|
||||
{
|
||||
/* are claims in this run evaluated anyway? */
|
||||
if (isRunTrusted(sys, rid))
|
||||
if (isRunTrusted (sys, rid))
|
||||
{ /* possibly claims to be checked in this run */
|
||||
rdscan = runPointerGet (sys, rid);
|
||||
while (rdscan != NULL)
|
||||
@ -1207,7 +1211,7 @@ claimViolationDetails (const System sys, const int run, const Roledef rd,
|
||||
{
|
||||
/* secrecy claim */
|
||||
|
||||
if (!isRunTrusted (sys,run))
|
||||
if (!isRunTrusted (sys, run))
|
||||
{
|
||||
/* claim was skipped */
|
||||
return (Termlist) - 1;
|
||||
@ -1236,6 +1240,10 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
|
||||
/* default = no adaption of pruning, continue search */
|
||||
flag = 1;
|
||||
|
||||
/* enough? */
|
||||
if (enoughAttacks (sys))
|
||||
return flag;
|
||||
|
||||
/* Count the violations */
|
||||
sys->attackid++;
|
||||
sys->failed = statesIncrease (sys->failed);
|
||||
@ -1328,7 +1336,7 @@ executeTry (const System sys, int run)
|
||||
if (runPoint->type == CLAIM)
|
||||
{
|
||||
/* first we might dynamically determine whether the claim is valid */
|
||||
if (!isRunTrusted (sys,run))
|
||||
if (!isRunTrusted (sys, run))
|
||||
{
|
||||
/* for untrusted agents we check no claim violations at all
|
||||
* so: we know it's okay. */
|
||||
|
@ -47,6 +47,7 @@ switchesInit (int argc, char **argv)
|
||||
switches.maxtracelength = INT_MAX;
|
||||
switches.runs = INT_MAX;
|
||||
switches.filterClaim = NULL; // default check all claims
|
||||
switches.maxAttacks = 0; // no maximum default
|
||||
|
||||
// Modelchecker
|
||||
switches.traverse = 12; // default traversal method
|
||||
@ -350,6 +351,21 @@ switcher (const int process, int index)
|
||||
}
|
||||
}
|
||||
|
||||
if (detect (' ', "max-attacks", 1))
|
||||
{
|
||||
if (!process)
|
||||
{
|
||||
/* not very important
|
||||
helptext ("--max-attacks=<int>", "when not 0, maximum number of attacks [0]");
|
||||
*/
|
||||
}
|
||||
else
|
||||
{
|
||||
switches.maxAttacks = integer_argument ();
|
||||
return index;
|
||||
}
|
||||
}
|
||||
|
||||
if (detect ('p', "prune", 1))
|
||||
{
|
||||
if (!process)
|
||||
|
@ -26,6 +26,7 @@ struct switchdata
|
||||
int maxtracelength; //!< Maximum trace length allowed
|
||||
int runs; //!< The number of runs as in the switch
|
||||
Term filterClaim; //!< Which claim should be checked?
|
||||
int maxAttacks; //!< When not 0, maximum number of attacks
|
||||
|
||||
// Modelchecker
|
||||
int traverse; //!< Traversal method
|
||||
|
20
src/system.c
20
src/system.c
@ -69,7 +69,7 @@ systemInit ()
|
||||
sys->untrusted = NULL;
|
||||
sys->secrets = NULL; // list of claimed secrets
|
||||
sys->synchronising_labels = NULL;
|
||||
sys->attack = NULL;
|
||||
sys->attack = NULL; // clash with prev. attack declaration TODO
|
||||
/* no protocols => no protocol preprocessed */
|
||||
sys->rolecount = 0;
|
||||
sys->roleeventmax = 0;
|
||||
@ -1216,7 +1216,7 @@ protocolsPrint (Protocol p)
|
||||
/**
|
||||
* 1 (True) means trusted, 0 is untrusted
|
||||
*/
|
||||
int
|
||||
int
|
||||
isAgentTrusted (const System sys, Term agent)
|
||||
{
|
||||
agent = deVar (agent);
|
||||
@ -1463,3 +1463,19 @@ system_iterate_roles (const System sys, int (*func) ())
|
||||
return 1;
|
||||
}
|
||||
|
||||
//! Determine whether we don't need any more attacks
|
||||
/**
|
||||
* Returns 1 (true) iff no more attacks are needed.
|
||||
*/
|
||||
int
|
||||
enoughAttacks (const System sys)
|
||||
{
|
||||
if (switches.maxAttacks != 0)
|
||||
{
|
||||
if (sys->attackid >= switches.maxAttacks)
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user