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

[Meta] ProVerif backend tracking issue #382

Open
2 of 11 tasks
jschneider-bensch opened this issue Dec 4, 2023 · 2 comments
Open
2 of 11 tasks

[Meta] ProVerif backend tracking issue #382

jschneider-bensch opened this issue Dec 4, 2023 · 2 comments
Assignees

Comments

@jschneider-bensch
Copy link
Contributor

jschneider-bensch commented Dec 4, 2023

This issue collects sub-tasks for the ProVerif backend.

  • Basic translation phases
    • Extract structs to generic concstructors
    • Extract ProVerif process macros from Rust fns
    • Extract ProVerif processes from annotated Rust fns
    • Automatic generation of generic top-level process
  • Rust component for ProVerif Processes #1129
    • Protocol runtime
  • hax-pv-lib ProVerif component (this let's us translate known API calls)
    • function definitions for libcrux APIs
    • state management facilities
  • When basic translation works: restrict Rust inputs to valid subset
@jschneider-bensch jschneider-bensch self-assigned this Dec 4, 2023
@franziskuskiefer franziskuskiefer moved this to In Progress in hax Dec 4, 2023
@jschneider-bensch
Copy link
Contributor Author

Tracking the more specific issues for the current milestone (Extracting the Bertie TLS handshake) in #541.

Copy link

github-actions bot commented Oct 4, 2024

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

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

No branches or pull requests

2 participants