Skip to content
GitLab
Commit 57c9f5fc authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Update

parent 59376c20
Hide whitespace changes
Inline Side-by-side
resources/models/tcp/win8client.dot 0 → 100644
View file @ 57c9f5fc
digraph G {
label=""
s0 [color="red"]
s1
s2
s3
s4
s5
s6
s7
s8
s9
s10
s11
s12
s0 [label="s0"];
s0 -> s0[label="ACK+RST(V,V,0)/TIMEOUT"]
s0 -> s2[label="CLOSE/TIMEOUT"]
s0 -> s1[label="CONNECT/SYN(FRESH,ZERO,0)"]
s0 -> s0[label="ACK+PSH(V,V,1)/TIMEOUT"]
s0 -> s0[label="SYN+ACK(V,V,0)/TIMEOUT"]
s0 -> s0[label="RST(V,V,0)/TIMEOUT"]
s0 -> s0[label="ACK(V,V,0)/TIMEOUT"]
s0 -> s0[label="FIN+ACK(V,V,0)/TIMEOUT"]
s0 -> s0[label="SYN(V,V,0)/TIMEOUT"]
s0 -> s0[label="RCV/TIMEOUT"]
s1 [label="s1"];
s1 -> s5[label="ACK+RST(V,V,0)/TIMEOUT"]
s1 -> s2[label="CLOSE/TIMEOUT"]
s1 -> s1[label="CONNECT/TIMEOUT"]
s1 -> s1[label="ACK+PSH(V,V,1)/TIMEOUT"]
s1 -> s4[label="SYN+ACK(V,V,0)/ACK(NEXT,NEXT,0)"]
s1 -> s5[label="RST(V,V,0)/TIMEOUT"]
s1 -> s1[label="ACK(V,V,0)/TIMEOUT"]
s1 -> s1[label="FIN+ACK(V,V,0)/TIMEOUT"]
s1 -> s3[label="SYN(V,V,0)/ACK+SYN(CURRENT,NEXT,0)"]
s1 -> s1[label="RCV/TIMEOUT"]
s2 [label="s2"];
s2 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s2 -> s2[label="CLOSE/TIMEOUT"]
s2 -> s2[label="CONNECT/TIMEOUT"]
s2 -> s2[label="ACK+PSH(V,V,1)/TIMEOUT"]
s2 -> s2[label="SYN+ACK(V,V,0)/TIMEOUT"]
s2 -> s2[label="RST(V,V,0)/TIMEOUT"]
s2 -> s2[label="ACK(V,V,0)/TIMEOUT"]
s2 -> s2[label="FIN+ACK(V,V,0)/TIMEOUT"]
s2 -> s2[label="SYN(V,V,0)/TIMEOUT"]
s2 -> s2[label="RCV/TIMEOUT"]
s3 [label="s3"];
s3 -> s0[label="ACK+RST(V,V,0)/TIMEOUT"]
s3 -> s2[label="CLOSE/RST(NEXT,CURRENT,0)"]
s3 -> s3[label="CONNECT/TIMEOUT"]
s3 -> s7[label="ACK+PSH(V,V,1)/ACK(NEXT,NEXT,0)"]
s3 -> s0[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s3 -> s0[label="RST(V,V,0)/TIMEOUT"]
s3 -> s4[label="ACK(V,V,0)/TIMEOUT"]
s3 -> s6[label="FIN+ACK(V,V,0)/ACK(NEXT,NEXT,0)"]
s3 -> s0[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s3 -> s3[label="RCV/TIMEOUT"]
s4 [label="s4"];
s4 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s4 -> s9[label="CLOSE/ACK+FIN(NEXT,CURRENT,0)"]
s4 -> s4[label="CONNECT/TIMEOUT"]
s4 -> s7[label="ACK+PSH(V,V,1)/ACK(NEXT,NEXT,0)"]
s4 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s4 -> s2[label="RST(V,V,0)/TIMEOUT"]
s4 -> s4[label="ACK(V,V,0)/TIMEOUT"]
s4 -> s6[label="FIN+ACK(V,V,0)/ACK(NEXT,NEXT,0)"]
s4 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s4 -> s8[label="RCV/TIMEOUT"]
s5 [label="s5"];
s5 -> s5[label="ACK+RST(V,V,0)/TIMEOUT"]
s5 -> s2[label="CLOSE/TIMEOUT"]
s5 -> s5[label="CONNECT/TIMEOUT"]
s5 -> s5[label="ACK+PSH(V,V,1)/RST(ZERO,ZERO,0)"]
s5 -> s5[label="SYN+ACK(V,V,0)/RST(ZERO,ZERO,0)"]
s5 -> s5[label="RST(V,V,0)/TIMEOUT"]
s5 -> s5[label="ACK(V,V,0)/RST(ZERO,ZERO,0)"]
s5 -> s5[label="FIN+ACK(V,V,0)/RST(ZERO,ZERO,0)"]
s5 -> s3[label="SYN(V,V,0)/ACK+SYN(FRESH,NEXT,0)"]
s5 -> s5[label="RCV/TIMEOUT"]
s6 [label="s6"];
s6 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s6 -> s10[label="CLOSE/ACK+FIN(NEXT,CURRENT,0)"]
s6 -> s6[label="CONNECT/TIMEOUT"]
s6 -> s6[label="ACK+PSH(V,V,1)/TIMEOUT"]
s6 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s6 -> s2[label="RST(V,V,0)/TIMEOUT"]
s6 -> s6[label="ACK(V,V,0)/TIMEOUT"]
s6 -> s6[label="FIN+ACK(V,V,0)/TIMEOUT"]
s6 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s6 -> s6[label="RCV/TIMEOUT"]
s7 [label="s7"];
s7 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s7 -> s2[label="CLOSE/ACK+RST(NEXT,CURRENT,0)"]
s7 -> s7[label="CONNECT/TIMEOUT"]
s7 -> s7[label="ACK+PSH(V,V,1)/ACK(NEXT,NEXT,0)"]
s7 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s7 -> s2[label="RST(V,V,0)/TIMEOUT"]
s7 -> s7[label="ACK(V,V,0)/TIMEOUT"]
s7 -> s11[label="FIN+ACK(V,V,0)/ACK(NEXT,NEXT,0)"]
s7 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s7 -> s4[label="RCV/TIMEOUT"]
s8 [label="s8"];
s8 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s8 -> s2[label="CLOSE/ACK+RST(NEXT,CURRENT,0)"]
s8 -> s8[label="CONNECT/TIMEOUT"]
s8 -> s4[label="ACK+PSH(V,V,1)/ACK(NEXT,NEXT,0)"]
s8 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s8 -> s2[label="RST(V,V,0)/TIMEOUT"]
s8 -> s8[label="ACK(V,V,0)/TIMEOUT"]
s8 -> s6[label="FIN+ACK(V,V,0)/ACK(NEXT,NEXT,0)"]
s8 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s8 -> s8[label="RCV/TIMEOUT"]
s9 [label="s9"];
s9 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s9 -> s9[label="CLOSE/TIMEOUT"]
s9 -> s9[label="CONNECT/TIMEOUT"]
s9 -> s2[label="ACK+PSH(V,V,1)/ACK+RST(NEXT,NEXT,0)"]
s9 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s9 -> s2[label="RST(V,V,0)/TIMEOUT"]
s9 -> s9[label="ACK(V,V,0)/TIMEOUT"]
s9 -> s12[label="FIN+ACK(V,V,0)/ACK(NEXT,NEXT,0)"]
s9 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s9 -> s9[label="RCV/TIMEOUT"]
s10 [label="s10"];
s10 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s10 -> s10[label="CLOSE/TIMEOUT"]
s10 -> s10[label="CONNECT/TIMEOUT"]
s10 -> s2[label="ACK+PSH(V,V,1)/TIMEOUT"]
s10 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s10 -> s2[label="RST(V,V,0)/TIMEOUT"]
s10 -> s2[label="ACK(V,V,0)/TIMEOUT"]
s10 -> s2[label="FIN+ACK(V,V,0)/TIMEOUT"]
s10 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s10 -> s10[label="RCV/TIMEOUT"]
s11 [label="s11"];
s11 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s11 -> s2[label="CLOSE/ACK+RST(NEXT,CURRENT,0)"]
s11 -> s11[label="CONNECT/TIMEOUT"]
s11 -> s11[label="ACK+PSH(V,V,1)/TIMEOUT"]
s11 -> s2[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s11 -> s2[label="RST(V,V,0)/TIMEOUT"]
s11 -> s11[label="ACK(V,V,0)/TIMEOUT"]
s11 -> s11[label="FIN+ACK(V,V,0)/TIMEOUT"]
s11 -> s2[label="SYN(V,V,0)/ACK+RST(ZERO,NEXT,0)"]
s11 -> s6[label="RCV/TIMEOUT"]
s12 [label="s12"];
s12 -> s2[label="ACK+RST(V,V,0)/TIMEOUT"]
s12 -> s12[label="CLOSE/TIMEOUT"]
s12 -> s12[label="CONNECT/TIMEOUT"]
s12 -> s12[label="ACK+PSH(V,V,1)/TIMEOUT"]
s12 -> s12[label="SYN+ACK(V,V,0)/RST(NEXT,FRESH,0)"]
s12 -> s2[label="RST(V,V,0)/TIMEOUT"]
s12 -> s12[label="ACK(V,V,0)/TIMEOUT"]
s12 -> s12[label="FIN+ACK(V,V,0)/TIMEOUT"]
s12 -> s12[label="SYN(V,V,0)/TIMEOUT"]
s12 -> s12[label="RCV/TIMEOUT"]
}
z3gi/learn/algorithm.py
View file @ 57c9f5fc
......@@ -3,6 +3,7 @@ from typing import List, Tuple, Union,cast
from model import Automaton
from learn import Learner
from model.fa import State
from model.ra import Action
from sut import StatsTracker, SUT, NoRstSUT
from sut.scalable import ActionSignature
......@@ -79,8 +80,22 @@ def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automa
done = False
break
return (model, statistics)
def learn_no_reset(sut:NoRstSUT, learner:Learner, max_inputs:int) -> Tuple[Union[Automaton, None], Statistics]:
import model
def _next_seq_rwalkfromstate(aut:Automaton, input_seq, rand_seq=3):
state = aut.state(input_seq)
acc_seq = model.get_trans_acc_seq(aut, from_state=state)
next_state = utils.rand_sel(list(acc_seq.keys()))
next_seq = acc_seq[next_state]
for _ in range(0, rand_seq):
tr = utils.rand_sel(aut.transitions(state))
state = tr.end_state
next_seq.append(tr)
return aut.trans_to_inputs(next_seq)
def _next_seq_rwalk(aut:Automaton, input_seq, rand_seq=3):
return [utils.rand_sel(aut.input_labels()) for _ in range(0, rand_seq)]
def learn_no_reset(sut:NoRstSUT, learner:Learner, max_inputs:int, rand_seq=3) -> Tuple[Union[Automaton, None], Statistics]:
""" takes a non-reseting SUL, a learner, a test generator, and a bound on the number of inputs and generates a model"""
trace = []
alpha = sut.input_interface()
......@@ -88,29 +103,41 @@ def learn_no_reset(sut:NoRstSUT, learner:Learner, max_inputs:int) -> Tuple[Union
statistics = Statistics()
trace.extend(sut.steps(seq))
learner.add(list(trace))
start_time = int(time.time() * 1000)
(hyp, definition) = learner.model()
end_time = int(time.time() * 1000)
statistics.add_learning_time(end_time - start_time)
done = False
while not done:
sim = get_no_rst_simulation(hyp)
sim.steps([inp for (inp,_) in trace])
inputs = [inp for (inp, _) in trace]
sim.steps(inputs)
next_inputs = _next_seq_rwalkfromstate(hyp, inputs, rand_seq=rand_seq)
done = True
for _ in range(0, max_inputs):
rand_inp = utils.rand_sel(alpha)
if len(next_inputs) == 0:
next_inputs = _next_seq_rwalkfromstate(hyp, inputs, rand_seq=rand_seq)
rand_inp = next_inputs.pop(0)
#rand_inp = utils.rand_sel(alpha)
out_sut = sut.step(rand_inp)
trace.append((rand_inp, out_sut))
inputs.append(rand_inp)
out_hyp = sim.step(rand_inp)
if out_sut != out_hyp:
learner.add(list(trace))
(hyp, definition) = learner.model(old_definition=definition)
start_time = int(time.time() * 1000)
ret = learner.model(old_definition=definition)
if ret is None:
return None, statistics
hyp,definition = ret
end_time = int(time.time() * 1000)
statistics.add_learning_time(end_time - start_time)
print("new hyp")
done = False
break
if hyp is None:
return None, None
statistics.inputs = len(trace) - max_inputs
return hyp, statistics
def learn_mbt(sut:SUT, learner:Learner, test_generator:TestGenerator, max_tests:int, stats_tracker:StatsTracker=None) -> Tuple[Union[Automaton, None], Statistics]:
""" takes learner, a test generator, and bound on the number of tests and generates a model"""
next_test = gen_blind_test(sut)
......
z3gi/learn/incremental/__init__.py 0 → 100644
View file @ 57c9f5fc
from abc import ABCMeta, abstractmethod
from typing import Tuple
import model
import define
class ILearner(metaclass=ABCMeta):
def __init__(self):
self.timeout = None
@abstractmethod
def add(self, trace):
pass
@abstractmethod
def model(self, old_definition:define.Automaton=None, old_model:model.Automaton=None) \
-> Tuple[model.Automaton, define.Automaton]:
""""Infers a minimal model whose behavior corresponds to the traces added so far.
Returns (None, to) if no model could be obtained where to suggests that learning failed due to
evaluation timing out"""
pass
def set_timeout(self, to):
"""sets the amount of time the solver is given for constructing a hypothesis"""
self.timeout = to
\ No newline at end of file
z3gi/learn/incremental/fa.py 0 → 100644
View file @ 57c9f5fc
from typing import Tuple
from z3 import z3
import define
from encode import IncrementalEncoder
from learn import Learner
from model import Automaton
class FAILearner(Learner):
def __init__(self, encoder:IncrementalEncoder, solver=None, verbose=False, stop_unknown=False):
super().__init__()
if not solver:
solver = z3.Solver()
self.solver = solver
self.encoder = encoder
self.verbose = verbose
self.stop_unknown = stop_unknown
self.cst = []
def add(self, trace):
trace_const = self.encoder.trace(trace)
#self.cst.append(trace_const)
self.solver.add(trace_const)
def model(self, min_states=1, max_states=20, old_definition:define.fa.FSM=None) -> Tuple[Automaton, define.fa.FSM]:
if old_definition is not None:
min_states = len(old_definition.states)
(succ, fa, m) = self._learn_model(min_states=min_states,
max_states=max_states)
if succ:
return fa.export(m), fa
else:
return None
def _learn_model(self, min_states=1, max_states=10):
"""generates the definition and model for an fa whose traces include the traces added so far
In case of failure, the second argument of the tuple signals occurrence of a timeout"""
for num_states in range(min_states, max_states + 1):
#self.solver.reset()
self.solver.add(z3.And(self.cst))
self.solver.push()
(states_const, aut_def) = self.encoder.automaton(num_states)
if self.timeout is not None:
self.solver.set("timeout", self.timeout)
self.solver.add(states_const)
result = self.solver.check()
if self.verbose:
print("Learning with {0} states. Result: {1}"
.format(num_states, result))
if result == z3.sat:
model = self.solver.model()
self.solver.pop()
return (True, aut_def, model)
else:
self.solver.pop()
# timeout
if result == z3.unknown and self.stop_unknown:
return (False, True, None)
# TODO: process the unsat core?
pass
return (False, False, None)
\ No newline at end of file
z3gi/model/__init__.py
View file @ 57c9f5fc
from abc import ABCMeta, abstractmethod
from typing import List
__all__ = [
"get_trans_acc_seq",
"get_prefix_tree",
"is_strongly_connected",
"defined_formalisms"
]
"""The most basic transition class available"""
......@@ -154,20 +161,11 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
def generate_acc_seq(self:Automaton, remove_unreachable=True):
"""generates access sequences for an automaton. It removes states that are not reachable."""
new_acc_seq = dict()
ptree = get_prefix_tree(self)
states = list(self.states())
for state in states:
pred = lambda x: (x.state == state)
node = ptree.find_node(pred)
if node is None:
print("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, self))
if remove_unreachable:
self._remove_state(state)
continue
#print("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, self))
#raise InvalidAutomaton
new_acc_seq[state] = node.path()
new_acc_seq = get_trans_acc_seq(self, from_state=self.start_state())
for state in self.states():
if state not in new_acc_seq and remove_unreachable:
self._remove_state(state)
assert(len(new_acc_seq) == len(self.states()))
self._acc_trans_seq = new_acc_seq
......@@ -229,7 +227,24 @@ def is_strongly_connected(aut : Automaton):
return True
def get_trans_acc_seq(aut : Automaton, from_state=None):
"""Generates transition access sequences for a given automaton"""
ptree = get_prefix_tree(aut, from_state=from_state)
acc_seq = dict()
states = list(aut.states())
for state in states:
pred = lambda x: (x.state == state)
node = ptree.find_node(pred)
if node is None:
print("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, aut))
continue
# print("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, self))
# raise InvalidAutomaton
acc_seq[state] = node.path()
return acc_seq
def get_prefix_tree(aut : Automaton, from_state=None):
"""Generates a transition prefix tree for a given automaton"""
visited = set()
to_visit = set()
if from_state is None:
......
z3gi/model/gen.py 0 → 100644
View file @ 57c9f5fc
from model.fa import MutableMealyMachine, IOTransition
import model
import utils
__all__ =[
"random_mealy"
]
def random_mealy(num_inputs:int, num_outputs:int, num_states:int, strongly_connected=True):
inp_alpha = ["I" + str(i+1) for i in range(0, num_inputs)]
out_alpha = ["O" + str(i+1) for i in range(0, num_outputs)]
states = ["q" + str(i+1) for i in range(0, num_states)]
while True:
mm = MutableMealyMachine()
for state in states:
mm.add_state(state)
for state in states:
for inp in inp_alpha:
r_out = utils.rand_sel(out_alpha)
r_state = utils.rand_sel(states)
tr = IOTransition(state, inp, r_out, r_state)
mm.add_transition(state, tr)
mm.generate_acc_seq()
machine = mm.to_immutable()
if len(machine.states()) == num_states:
if not strongly_connected or model.is_strongly_connected(machine):
return machine
z3gi/yan_benchmark.py
View file @ 57c9f5fc
......@@ -35,8 +35,8 @@ def get_learner_setup(aut:Automaton, test_desc:TestDesc):
cache = IOCache( MealyObservation)
sut = CacheSUT(stats_sut, cache)
learner = FALearner(MealyEncoder())
#tester = TestGeneratorChain([ColoringTestGenerator(sut, cache), MealyRWalkFromState(sut, rand_start_state=True, rand_length=test_desc.rand_length, prob_reset=0.2)])
tester = MealyRWalkFromState(sut, rand_start_state=True, rand_length=test_desc.rand_length, prob_reset=0.1)
tester = TestGeneratorChain([ColoringTestGenerator(sut, cache), YannakakisTestGenerator(sut, max_k=test_desc.max_k, rand_length=test_desc.rand_length)])
#tester = MealyRWalkFromState(sut, rand_start_state=True, rand_length=test_desc.rand_length, prob_reset=0.1)
#tester = YannakakisTestGenerator(sut, max_k=test_desc.max_k, rand_length=test_desc.rand_length)#])
return (learner, tester, sut, sut_stats)
......@@ -121,6 +121,7 @@ b = Benchmark()
models_path = os.path.join("..", "resources", "models")
bankcards_path = os.path.join(models_path, "bankcards")
pdu_path = os.path.join(models_path, "pdu")
tcp_path = os.path.join(models_path, "tcp")
biometric = ModelDesc("biometric", "MealyMachine", os.path.join(models_path, "biometric.dot"))
bankcard_names= ["MAESTRO", "MasterCard", "PIN", "SecureCode", "VISA"]
......@@ -128,22 +129,30 @@ bankcard_names= ["MAESTRO", "MasterCard", "PIN", "SecureCode", "VISA"]
bankcards = [ModelDesc(name, "MealyMachine", os.path.join(bankcards_path, "{}.dot".format(name))) for name in bankcard_names]
pdus = [ModelDesc("pdu" + str(i), "MealyMachine",
os.path.join(pdu_path, "model{}.dot".format(i))) for i in range(1,7)]
tcpclient = ModelDesc("win8client", "MealyMachine", os.path.join(tcp_path, "win8client.dot"))
#b.add_experiment(bankcards[-1)
#for pdu in pdus[-2:]:
#b.add_experiment(biometric)
#for bankcard in bankcards:
# b.add_experiment(bankcard)
#for pdu in pdus:
# b.add_experiment(pdu)
b.add_experiment(tcpclient)
#b.add_experiment(bankcards[-1])
b.add_experiment(biometric)
#b.add_experiment(bankcards[1])
#b.add_experiment(biometric)
#b.add_experiment(biometric)
#b.add_experiment(bankcards[-1])
#b.add_experiment(pdus[-1])
#b.add_experiment(pdus[-2])
# create a test description
t_desc = TestDesc(max_tests=10000, max_k=3, rand_length=3)
t_desc = TestDesc(max_tests=10000, max_k=1, rand_length=1)
# give the smt timeout value (in ms)
timeout = 60000
# how many times each experiment should be run
num_exp = 5
num_exp = 2
# run the benchmark and collect results
results = []
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment