Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Integration of Porridge] Generalized POR #19

Open
wants to merge 61 commits into
base: master
Choose a base branch
from

Conversation

LCBH
Copy link

@LCBH LCBH commented Jul 23, 2018

This PR integrates the library Porridge (see companion paper) into DeepSec.

Compared to the built-in POR techniques already implemented in DeepSec, Porridge provides a new POR technique that can be applied to any process (instead of action-determinate processes) but whose reduction, in terms of removal of traces, is often much less important. Unfortunately for now, the pre-computation handled by Porridge can be impractically long for large processes. Furthermore, some syntactical conditions over the input processes mut be fulfilled (this is only for easing the integration), most of them are checked at runtime. Therefore, Porridge is opt-in: one needs to use the option -with_por_gen. All concerned options are labeled Experimental.

This PR includes:

  • the library Porridge in the folder porridge/,
  • an interface between processes and traces as represented in DeepSec and as represented in Porridge: Source/core_library/por.ml (some .mli had to be modified),
  • an integration of the search restriction guided by Porridge: Source/subterms/equivalence*.ml*,
  • new installation instructions (README.md),
  • some debugging utilities have been modified/improved,
  • new examples in Examples/POR_gen/ (those examples are discussed in the ESORICS'18 paper).

Lucca Hirschi and others added 30 commits January 22, 2018 16:52
TODO: fix differences of interfaces
Now works except for distributed computing.
Todo: distributed computing + POR.
-> does not seem to be the case though
-> TODO: fix that
…works now

+ add debug options in Source/distributed/distrib.ml -> each worker logs in a different file
P and Q~ have same structure (equal up to term, excluding channels).
@LCBH
Copy link
Author

LCBH commented Jul 23, 2018

The commit 8113253 can be reversed if you actually like the output line (Stats) ---- Number of explorations [118]., even when generalized POR is disabled.

@VincentCheval
Copy link
Member

A new version of Deepsec is coming very soon. So I'm thinking of merging Porridge for this new version.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants