Commit 8b669ab1 authored by Andrew's avatar Andrew
Browse files

Merge branch 'opacity_enf' of https://gitlab.eecs.umich.edu/M-DES-tools/desops into opacity_enf

parents f9f35e07 01970425
The files in this folder contain functions related to enforcing opacity using the reactive synthesis tool BoSy (https://github.com/reactive-systems/bosy)
The main function to perform run the full synthesis process is run_bosy() in bosy_interface.py
Some modifications must be made to the base BoSy installation so that it uses a Buchi automaton we construct, instead of converting an LTL specification to a Buchi automaton.
There are two changed files in the swift_files folder within this directory that must be copied into the BoSy installation:
- Conversion.swift should be copied into {bosy_path}/Sources/Automata/Conversion.swift (overwriting the existing file)
- main.swift should be copied into {bosy_path}/Sources/BoSyHyper/main.swift (overwriting the existing file)
### BoSy Installation
In an directory external to M-DESops, clone the correct commit of BoSy with
$ git clone https://github.com/reactive-systems/bosy.git
$ git checkout 2bad0d853e1b023aa27a6a0d8f8a129b5bd96ed7
The main function to perform run the full synthesis process is run_bosy() in bosy_interface.py
Copy the file `bosy_patch.patch` in this directory of M-DESops into the newly created `bosy/` directory.
In the `bosy/` directory, apply the patch with the command
$ git apply bosy_patch.patch
Next, BoSy can be installed as usual. See instructions at https://github.com/reactive-systems/bosy. If the necessary dependencies (i.e. swift) are installed, this can typically be done with the command `make`.
......@@ -20,7 +20,7 @@ from DESops.opacity.bosy.spin import ltl2spin, read_spin, write_spin
# Change the path to Bosy here appropriately
bosy_path = "/".join([str(Path.home()), "libraries/bosy"])
# Also ensure that Aiger is installed at the following path
aiger_path = "/".join([str(Path.home()), "libraries/aiger-1.9.9"])
aiger_path = "/".join([str(Path.home()), "libraries/aiger"])
# Note there are currently some issues with non-absolute paths
......@@ -167,17 +167,20 @@ def run_bosy(
)
def synthesize_bosy(bosy_path, aag_path):
def synthesize_bosy(i_bosy_path, i_aag_path):
"""
Synthesize a controller from hyperLTL specifications using bosy.
Parameters:
bosy_path: the path for the input bosy file
aag_path: the path for the Aiger (.aag) file
i_bosy_path: the path for the input bosy file
i_aag_path: the path for the Aiger (.aag) file
"""
print(os.popen("echo $PATH").read())
#print(os.popen("echo $PATH").read())
#os.system(
# f"swift run -c release BoSyHyper --synthesize {i_bosy_path} | sed -ne '/^aag.*/,$ p' > {i_aag_path}"
#)
os.system(
f"swift run -c release BoSyHyper --synthesize {bosy_path} | sed -ne '/^aag.*/,$ p' > {aag_path}"
f".build/release/BoSyHyper --synthesize {i_bosy_path} | sed -ne '/^aag.*/,$ p' > {i_aag_path}"
)
......
commit 7aeca375e86946c2d3c395248bb549a9abaa9cc0
Author: Andrew Wintenberg <awintenb@umich.edu>
Date: Thu May 5 11:56:37 2022 -0400
Customization for M-DESops
diff --git a/Sources/Automata/Conversion.swift b/Sources/Automata/Conversion.swift
index 6196783..73a83cc 100644
--- a/Sources/Automata/Conversion.swift
+++ b/Sources/Automata/Conversion.swift
@@ -20,6 +20,8 @@ public enum LTL2AutomatonConverter {
return "ltl3ba"
case .spot(_):
return "spot"
+ case .input:
+ return "input"
}
}
@@ -29,10 +31,12 @@ public enum LTL2AutomatonConverter {
return try convertWithLtl3ba(ltl: ltl)
case let .spot(cliOpts):
return try convertWithSpot(ltl: ltl, hoaf: false, cliOpts: cliOpts)
+ case let .input:
+ return try useInputFile()
}
}
- public static let allValues: [LTL2AutomatonConverter] = [.ltl3ba, .spot("")]
+ public static let allValues: [LTL2AutomatonConverter] = [.ltl3ba, .spot(""), .input]
}
public func initAutomatonConverter(_ name: String, args: String) throws -> LTL2AutomatonConverter{
@@ -41,6 +45,8 @@ public func initAutomatonConverter(_ name: String, args: String) throws -> LTL2A
return LTL2AutomatonConverter.spot(args)
case "ltl3ba":
return LTL2AutomatonConverter.ltl3ba
+ case "input":
+ return LTL2AutomatonConverter.input
default:
throw ParseError.toolNotFound(name) //throw error here, fix later
}
@@ -75,6 +81,12 @@ func convertWithSpot(ltl: LTL, hoaf: Bool = false, cliOpts: String = "") throws
}
}
+func useInputFile() throws -> CoBüchiAutomaton {
+ let in_file = URL(fileURLWithPath: FileManager().currentDirectoryPath).appendingPathComponent("in.spin")
+ let input = try! String(contentsOf: in_file)
+ return try parseSpinNeverClaim(neverClaim: input)
+}
+
func parseSpinNeverClaim(neverClaim: String) throws -> CoBüchiAutomaton {
var states: Set<String> = Set()
var rejectingStates: Set<String> = Set()
diff --git a/Sources/BoSyHyper/main.swift b/Sources/BoSyHyper/main.swift
index f0e99e4..4d75b07 100644
--- a/Sources/BoSyHyper/main.swift
+++ b/Sources/BoSyHyper/main.swift
@@ -69,7 +69,7 @@ do {
if !searchEnvironment {
// build automaton for linear
- guard let linearAutomaton = try? CoBüchiAutomaton.from(ltl: !linear, using: .spot("")) else {
+ guard let linearAutomaton = try? CoBüchiAutomaton.from(ltl: !linear, using: .input) else {
Logger.default().error("could not construct automaton")
fatalError()
}
import datetime
import os
import DESops as d
from DESops.opacity.bosy.bosy_interface import run_bosy
from DESops.opacity.bosy.parse_smv import read_smv
from DESops.opacity.bosy.verify import verify_edit_function
from DESops.opacity.contact_tracing.generate_contact_model import contact_example
# choose between running full synthesis, or just parsing existing SMV file
run_synthesis = True
# choose between custom LTL or standard always inference
use_ltl = False
# choose whether we should attempt to simplify transitions using SymPy
simplify = False
if not os.path.exists('contact'):
os.makedirs('contact')
# model parameters
map_file = "map1.fsm"
num_agents = 2
ids = list(range(num_agents))
pairs = [str(i) + str(j) for i in ids for j in ids if i < j]
base_path = "contact/cntl"
# generate and save model
g, event_var_maps = contact_example(map_file, num_agents)
d.write_fsm("contact/sys.fsm", g)
events = sorted(list(g.events))
inf_vars = [f"c_{p}" for p in pairs]
if use_ltl:
# generate LTL expression that requires that contact is eventually inferred
inf_fun = None
ltl_spec = list()
for p in pairs:
inf_var = f"c_{p}"
contact_events = [e for e in events if p in e]
ltl_spec.append(f"(!{inf_var} W ({' || '.join(contact_events)}))")
ltl_spec.append(f"(F({' || '.join(contact_events)}) -> F({inf_var}))")
else:
# generate functions that return inferences about whether the current event includes a specific contact pair
ltl_spec = None
inf_fun = list()
for p in pairs:
inf_var = f"c_{p}"
inf_fun.append(lambda x, e: f"{inf_var}" if p in e else f"!{inf_var}")
# generate valid replacements sets for each event
valid_replaces = dict()
for e_i in events:
# observer location should match
valid_replaces[e_i] = {e_o for e_o in events if e_o[1] == e_i[1]}
if run_synthesis:
os.environ["PATH"] += os.pathsep + "/usr/local/swift/bin/"
print(f"Synthesis start: {datetime.datetime.now()}\n")
cntl, preds = run_bosy(
base_path,
g,
ltl_spec=ltl_spec,
event_var_maps=event_var_maps,
inf_fun=inf_fun,
inf_vars=inf_vars,
ins_bound=1,
valid_replaces=valid_replaces,
)
print(f"Synthesis end: {datetime.datetime.now()}\n")
else:
cntl, preds = read_smv(
f"{base_path}.smv",
g,
event_var_maps,
inf_vars,
allow_insert=False,
insert_holds_events=True,
)
success = verify_edit_function(g, cntl)
if success:
print("Successful obfuscation")
else:
print("Obfsucation failed")
# save output automata
d.write_fsm(base_path + ".fsm", cntl)
for inf, pred in preds.items():
pred.vs["marked"] = pred.vs["secret"]
d.write_fsm(f"contact/pred_{inf}.fsm", pred)
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