YoVDO

Formally Verifying Everybody's Cryptography

Offered By: Strange Loop Conference via YouTube

Tags

Strange Loop Conference Courses Cryptography Courses Cryptographic Primitives Courses Software Security Courses Formal Verification Courses Threat Models Courses

Course Description

Overview

Explore formal verification of cryptographic libraries in this conference talk from Strange Loop 2022. Learn how mathematical reasoning can prove code security and bug-free status in real-world cryptographic systems. Discover the application of formal verification to production cryptography, its cost-effectiveness as an assurance tool, and lessons for securing other software systems. Delve into the threat model for cryptographic primitives, understand the challenges and benefits of verifying cryptography, and examine practical examples such as SHA 384 rewrites. Gain insights into cumulative correctness planning and the power of code changes during formal verification processes.

Syllabus

Intro
Aim: formal verification of code
This talk: cryptographic primitives
Who did the proofs, anyway?
We do difficult proofs
Threat model for cryptographic primitives
So, verification is just fancy testing
Result-high confidence of this
Verifying cryptography is easy! (in some ways)
Conservation of difficulty rule
Why is it difficult to verify cryptography?
Verifying cryptography is difficult, as well
Changing the code is very powerful during formal verification!
Rewrites in practice (from SHA 384)
Composition has a cost
Cumulative Correctness planning


Taught by

Strange Loop Conference

Tags

Related Courses

Secure Software Development Fundamentals
Linux Foundation via edX
Security Literacy Course (How To)
Treehouse
Lessons Learned from Evaluating the Robustness of Defenses to Adversarial Examples
Simons Institute via YouTube
Security Protection and Quality Control in Crowdsourcing
CAE in Cybersecurity Community via YouTube
Cross-App Poisoning in Software-Defined Networking
Association for Computing Machinery (ACM) via YouTube