Universally Composable Formal Methods Summer School

Registration is now open for a free Universally Composable (UC) formal methods “summer school” from Aug. 11-14 at Boston University.

This event is geared toward researchers and engineers seeking to understand how the UC formal methods ecosystem can enhance the resilience of software systems to cyber threats and attacks. The event is also suitable for researchers seeking to understand and build upon recent advancements in the underlying formal methods theory, thereby potentially scaling the ecosystem to whole-system resiliency and beyond.

The four-day summer school is organized into two halves:

• Aug. 11-12: Attendees learn how to use the UC ecosystem to model, analyze, and prove real-world protocols inspired by DARPA’s HARDEN program.
• Aug. 13 - 14:^* In breakout sessions, attendees are encouraged to push the envelope within specific communities of interest.
  
  ^*While these breakout sessions are optional, they are encouraged for attendees to provide valuable feedback on real-world problems and priorities that could guide research trajectories.

Seating is limited, and registration is available on a first-come, first-served basis. An online option (e.g., via Zoom) is also available for those who are unable to attend in person.

Read the agenda and register

About

Riverside Research is co-hosting this summer school as part of our Hardening Development Toolchains Against Emergent Execution Engines (HARDEN) program. The event aligns with the broader Resilient Software Systems initiative.

HARDEN seeks to develop practical tools to anticipate, isolate, and mitigate emergent behaviors (behaviors that can be created using expected and unexpected behaviors) in computing systems throughout the entire software development lifecycle.

Through HARDEN, Riverside Research’s Universal Composability for Preventing Adversarial Composition Techniques (UC-PACT) effort is making software system modeling easier by allowing users to graphically design software system models. UC-PACT models represent both an idealized (expected) secure design and the actual implementation (may contain expected and unexpected behaviors). These UC ecosystem tools are used to prove the nonexistence of emergent behaviors.