Commit 0fb1d99a authored by matblisc's avatar matblisc
Browse files

added language-based method for verifying separate K-step opacity

parent d2e178c2
......@@ -22,6 +22,9 @@ def inplace_reverse(g):
Constructs the reverse of the given automaton in-place
"""
g.vs["init"] = True
if g.ecount() == 0:
return
t = g.es[0]
for _ in range(g.ecount()):
g.add_edge(t.target, t.source, t["label"])
......
......@@ -39,10 +39,10 @@ def contract_secret_traces(g, h, Euo, any_nonsec_is_nonsec):
R.update([e.target for e in g.es.select(label_notin=Euo)])
Rlist = list(R)
h.add_vertices(
len(R), [(ind, 1) for ind in R]
) # names must be in this form for verify_joint_k_step_opacity_alternative
# names must be in this form for verify_joint_k_step_opacity_alternative
h.add_vertices(len(R), [(ind, 1) for ind in R])
h.add_vertices(len(R), [(ind, 0) for ind in R])
h.vs.select(range(len(R)))["orig_vert"] = Rlist
h.vs.select(range(len(R)))["secret"] = True
h.vs.select(range(len(R), 2 * len(R)))["orig_vert"] = Rlist
......
"""
Functions related to the alternative method for k-step and infinite-step opacity that is based on language inclusion
"""
import igraph as ig
from DESops import Automata
from DESops.Automata import product_comp
from DESops.basic.product_NFA import product_NFA
from DESops.opacity.contract_secret_traces import contract_secret_traces
......@@ -21,18 +23,15 @@ def verify_joint_k_step_opacity_alternative(g, k):
Euo = g.Euo
Eo = set(g.es["label"]).difference(Euo)
g_contracted = Automata()
contract_secret_traces(g, g_contracted, Euo, False)
g_c = Automata()
contract_secret_traces(g, g_c, Euo, False)
g_contracted.reverse(inplace=True)
g_contracted.vs["marked"] = [
g.vs[i]["init"] for i in [state[0] for state in g_contracted.vs["name"]]
]
g_contracted.vs["secret"] = [v["name"][1] for v in g_contracted.vs]
g_c.reverse(inplace=True)
g_c.vs["marked"] = [g.vs[state[0]]["init"] for state in g_c.vs["name"]]
h = construct_unfolded_automaton(g_contracted, g.vs, k)
h = construct_reverse_unfolded_automaton(g_c, g.vs, k)
return language_inclusion(g_contracted, h, Eo)
return language_inclusion(g_c, h, Eo)
def verify_joint_infinite_step_opacity_alternative(g):
......@@ -46,29 +45,44 @@ def verify_joint_infinite_step_opacity_alternative(g):
Euo = g.Euo
Eo = set(g.es["label"]).difference(Euo)
g_contracted = Automata()
contract_secret_traces(g, g_contracted, Euo, False)
g_contracted.vs["marked"] = [
g.vs[i]["init"] for i in [state[0] for state in g_contracted.vs["name"]]
]
g_contracted.vs["secret"] = [v["name"][1] for v in g_contracted.vs]
g_c = Automata()
contract_secret_traces(g, g_c, Euo, False)
g_c.vs["marked"] = [g.vs[state[0]]["init"] for state in g_c.vs["name"]]
h = g_c.copy()
h._graph.delete_vertices([v for v in h.vs if v["secret"]])
h.vs["marked"] = True
return language_inclusion(g_c, h, Eo)
h = g_contracted.copy()
h._graph.delete_vertices([v for v in g.vs if v["secret"]])
return language_inclusion(g_contracted, h, Eo)
def min_k_for_joint_opacity_violation(g):
"""
Returns the minimum value of K for which the automaton g is not joint K-step opaque
"""
if verify_joint_infinite_step_opacity_alternative(g):
return float("inf")
k = 0
while True:
if not verify_joint_k_step_opacity_alternative(g, k):
return k
k += 1
def construct_unfolded_automaton(g_r, g_vs, k):
def construct_reverse_unfolded_automaton(g_r, g_vs, k):
"""
Returns the "unfolded" automaton that follows the reverse automaton but
avoids visiting any secret states within the first K steps
Used for verifying joint K-step opacity
g_r: the reverse contracted automaton
g_vs: the vertex sequence of the original automaton g
k: the number of steps
"""
h = Automata()
# start with nonsecret states 0 steps from the end
S0 = [((v, 0), 0) for v in g_vs.select(secret=False).indices]
state_indices = dict()
for state in S0:
......@@ -81,10 +95,14 @@ def construct_unfolded_automaton(g_r, g_vs, k):
state = need_to_check.pop()
if g_r.vs.select(name=state[0]):
for t in g_r.vs.select(name=state[0])[0].out_edges():
if state[1] == k:
step = state[1]
# if already k steps from the end, we can go to the next state even if it's secret
if step == k:
next_state = (t.target_vertex["name"], k)
# we can go to secret states within K steps from the end
elif not t.target_vertex["secret"]:
next_state = (t.target_vertex["name"], state[1] + 1)
next_state = (t.target_vertex["name"], step + 1)
# we can't go to a secret state within K steps from the end
else:
continue
......@@ -95,23 +113,113 @@ def construct_unfolded_automaton(g_r, g_vs, k):
h.add_edge(state_indices[state], state_indices[next_state], t["label"])
# fix added states having None instead of False for init attribute
h.vs["init"] = [(True if state["init"] else False) for state in h.vs]
# states are marked if they are initial in the original g
h.vs["marked"] = [g_vs[state[0][0]]["init"] for state in h.vs["name"]]
return h
def verify_separate_k_step_opacity_alternative(g, k):
"""
Returns whether the given automaton with unobservable events and secret states is joint k-step opaque
Parameters:
g: the automaton
k: the number of steps
"""
Euo = g.Euo
Eo = set(g.es["label"]).difference(Euo)
g_c = Automata()
contract_secret_traces(g, g_c, Euo, True)
g_c.vs["marked"] = True
# add self loops to each state so that runs reaching a dead state can be extended
g_c.add_edges([(i, i) for i in range(g_c.vcount())], ["e_self"] * g_c.vcount())
h = construct_forward_unfolded_automaton(g_c, k)
return language_inclusion(g_c, h, Eo)
def construct_forward_unfolded_automaton(g_c, k):
"""
Returns the "unfolded" automaton that follows the forward automaton but
avoids visiting any secret states within the last K steps
Used for verifying separate K-step opacity
g_c: the contracted automaton
g_vs: the vertex sequence of the original automaton g
k: the number of steps
"""
h = Automata()
# start with initial states of g_c at each step in {0,...K}
S0 = [(state["name"], i) for state in g_c.vs if state["init"] for i in range(k + 1)]
state_indices = dict()
for state in S0:
state_indices[state] = h.vcount()
h.add_vertex(state)
h.vs["init"] = True
need_to_check = S0
while need_to_check:
state = need_to_check.pop()
if g_c.vs.select(name=state[0]):
for t in g_c.vs.select(name=state[0])[0].out_edges():
step = state[1]
next_states = list()
# if >=K steps until the end we can always stay at >=K steps
if step == k:
next_states.append((t.target_vertex["name"], k))
# only nonsecret states can go from K to K-1 steps from the end
if step > 0 and not t.source_vertex["secret"]:
next_states.append((t.target_vertex["name"], k - 1))
# between 1 and K-1 steps from the end we can visit any state
elif step > 0:
next_states.append((t.target_vertex["name"], step - 1))
while next_states:
next_state = next_states.pop()
if next_state not in state_indices:
state_indices[next_state] = h.vcount()
h.add_vertex(next_state)
need_to_check.append(next_state)
h.add_edge(
state_indices[state], state_indices[next_state], t["label"]
)
# fix added states having None instead of False for init attribute
h.vs["init"] = [(True if state["init"] else False) for state in h.vs]
# for K=0, all states are at step K so we need to mark the nonsecret ones
if k == 0:
h.vs["marked"] = [(state[0][1] == 0) for state in h.vs["name"]]
# for K>0 we mark any state that reached step 0
else:
h.vs["marked"] = [(state[1] == 0) for state in h.vs["name"]]
return h
def language_inclusion(g, h, Eo):
"""
Returns whether the language marked by g is a subset of the language marked by h
Requires that the event sets are the same for both automata
Note: Only use this if the event sets are the same for both automata
g, h: the two automata
Eo: the set of observable events
"""
g_det = g.observer(save_marked_states=True)
h_det = h.observer(save_marked_states=True)
h_det.complement(events=Eo, inplace=True)
prod = product_comp([g_det, h_det], save_marked_states=True)
P = ig.Graph(directed=True)
product_NFA(P, [g, h_det], save_state_names=True, save_marked_states=True)
prod = Automata(P)
for v in prod.vs:
if v["marked"]:
......
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