GitHub - thedevilhimselfcodes/CertAlloc · GitHub
/" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
/;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
thedevilhimselfcodes
CertAlloc
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star
main
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>10 Commits<br>10 Commits
benchmark
benchmark
compliance
compliance
docs
docs
include
include
lib
lib
tools
tools
readme.md
readme.md
View all files
Repository files navigation
CertAlloc: Formally Verified Memory Suite
CertAlloc is a high-performance, $O(1)$ constant-time pool memory allocator designed for safety-critical embedded systems. Unlike standard malloc, CertAlloc is architected to be deterministic, thread-safe, and formally verified against memory corruption.
🚀 Key Features
Formal Proofs: Architecturally verified via TLA+; C-code logic verified via CBMC.
$O(1)$ Performance: Constant-time allocation and deallocation using hardware-accelerated bitwise intrinsics.
Safety-Ready: Built-in hardware critical section hooks for bare-metal (AVR/ARM) and POSIX (Linux/WSL) environments.
Audit-Ready: Includes a full suite of verification artifacts, including formal proof logs and stress-test benchmarks.
🛠️ Repository Structure
include/: Public API header (certalloc.h).
lib/: Compiled static library (libcertalloc.a).
tools/: Compiled static analyzer binary (certalloc-analyzer).
compliance/: Formal proof logs (TLA+ and CBMC) and benchmark reports.
📋 Integration Instructions
1. Linking the Library
To use CertAlloc in your project, link the static library and include the public header:
# Example compilation command<br>gcc main.c -L./lib -lcertalloc -I./include -o product_app -pthread
2. Implementation
Initialize the allocator before performing any memory operations:
#include "certalloc.h"
int main() {<br>if (certalloc_init()) {<br>void* ptr = cert_alloc(16);<br>// ... perform operations ...<br>cert_free(ptr);<br>return 0;
🧪 Verification & Testing
Integration Validation
To verify the library is correctly linked and functional in your environment:
Create a test_harness.c calling certalloc_init(), cert_alloc(), and cert_free().
Compile using the instructions above.
If the binary executes without segmentation faults, the library is correctly integrated.
Static Memory Bounding
Use the provided certalloc-analyzer tool to scan your source tree and calculate the maximum theoretical memory requirements for your application:
./tools/certalloc-analyzer
🔒 Verification Evidence
This library comes with a pre-computed "Verification"
Drop me a whatsApp via +94 76 388 5727 or mail me at vindana@cyburndigital.com for proof. Only if you are interested.
TLA+ Proofs: Proving architectural impossibility of deadlocks or double-allocations.
CBMC Proofs: Mathematical guarantee of zero buffer overflows or pointer alignment risks.
Stress Test Logs: Validated performance under 1,000,000 randomized operations with 0% memory leakage.
⚖️ License & Compliance
This software is provided as a Production-Ready Component . Please refer to the compliance/ documentation for TLA+, CBMC Proof when submitting this component for internal audits or external safety certifications (ISO 26262/IEC 62304). For licensing, please contact mailtovindana@gmail.com, vindana@cyburndigital.com, +94 76 388 5727 (WhatsApp).
About
No description, website, or topics provided.
Resources
Readme
Uh oh!
There was an error while loading. Please reload this page.
Activity
Stars
stars
Watchers
watching
Forks
forks
Report repository
Releases
No releases published
Packages
Uh oh!
There was an error while loading. Please reload this page.
Contributors
Uh oh!
There was an error while loading. Please reload this page.
Languages
100.0%
You can’t perform that action at this time.