Name
Abstract | ||
|---|---|---|
We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number of participating agents. The information flow policies are specified in a temporal logic for hyperproperties. We show that the verification problem can be reduced to the satisfiability of a formula of first-order linear-time temporal logic, and provide decidability results for relevant classes of workflows and specifications. We report on experimental results obtained with an implementation of our approach on a series of benchmarks.
|
Year | DOI | Venue |
|---|---|---|
2017 | 10.1145/3133956.3134080 | CCS |
DocType | Volume | ISBN |
Journal | abs/1708.09013 | 978-1-4503-4946-8 |
Citations | PageRank | References |
4 | 0.41 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernd Finkbeiner | 1 | 666 | 69.95 |
| Christian Müller | 2 | 13 | 1.92 |
| Helmut Seidl | 3 | 1468 | 103.61 |
| Eugen Zalinescu | 4 | 130 | 9.40 |