juniper/TinyCrypT
1
0
Fork 0
Code Issues 10 Pull requests Projects 1 Releases Packages Wiki Activity Actions

Full memory and UB soundness proofs #1

New issue
Open
opened 2026-08-06 00:19:11 +00:00 by juniper · 1 comment
juniper commented 2026-08-06 00:19:11 +00:00
Owner
Copy link

Memory and UB soundness proofs on all library code using Frama-C and WP.

Memory and UB soundness proofs on all library code using Frama-C and WP.
juniper self-assigned this 2026-08-06 00:28:10 +00:00
juniper commented 2026-08-12 01:20:03 +00:00
Author
Owner
Copy link

Switched to CBMC due to interacting better with GNU vector extensions. Soundness proof system set up and passing for SHA-3: 28ba9f7ca3

Switched to CBMC due to interacting better with GNU vector extensions. Soundness proof system set up and passing for SHA-3: https://forge.eyes-like-fire.org/juniper/TinyCrypT/commit/28ba9f7ca37591d364ed25178a99e8fe871c91e0
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
unity-tests
No results found.
Labels
Clear labels   
Compat/Breaking
Breaking change that won't be backward compatible

  
Kind/Bug
Something is not working

  
Kind/Documentation
Documentation changes

  
Kind/Enhancement
Improve existing functionality

  
Kind/Feature
New functionality

  
Kind/Security
This is security issue

  
Kind/Testing
Issue or pull request related to testing

  
Priority
Critical
 The priority is critical

  
Priority
High
 The priority is high

  
Priority
Low
 The priority is low

  
Priority
Medium
 The priority is medium

  
Reviewed
Confirmed
 Issue has been confirmed

  
Reviewed
Duplicate
 This issue or pull request already exists

  
Reviewed
Invalid
 Invalid issue

  
Reviewed
Won't Fix
 This issue won't be fixed

  
Status
Abandoned
 Somebody has started to work on this but abandoned work

  
Status
Blocked
 Something is blocking this issue or pull request

  
Status
Need More Info
 Feedback is required to reproduce issue or to continue work

No labels
Compat/Breaking
Kind/Bug
Kind/Documentation
Kind/Enhancement
Kind/Feature
Kind/Security
Kind/Testing
Priority
Critical
Priority
High
Priority
Low
Priority
Medium
Reviewed
Confirmed
Reviewed
Duplicate
Reviewed
Invalid
Reviewed
Won't Fix
Status
Abandoned
Status
Blocked
Status
Need More Info
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
1.0.0 Stable Release
Assignees
Clear assignees
No assignees
juniper
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
juniper/TinyCrypT#1
No description provided.