Posts tagged #python
-
Verified Security Gates: Safe ML Deserialization
Using Lean 4 soundness proofs to gate Python type-stub deserialization in the Falcon-secure project.
-
Lean 4 as a Soundness Oracle for Security Properties
Type stubs catch misuse at type-check time. But can we prove they are sound — that a well-typed program cannot trigger the dangerous code path? Enter Lean 4.
-
Pickle Is a CVE Factory; Type Stubs Are the Gate
Every ML project eventually loads a pickle file. This is a problem: pickle can execute arbitrary Python on deserialization. Here is how falcon-secure uses Python type stubs to make unsafe loads a static type error.
-
From Bug Fix to Production Hardening: A Refactoring Marathon
Stalled task detection, security hardening, code refactoring, and lifecycle signals — turning a task queue into production-grade infrastructure.
-
Pessimistic Locking: One Task, One Worker
Using SELECT FOR UPDATE SKIP LOCKED to prevent multiple workers from claiming the same task — database-level concurrency without application-level locks.
-
The Fork, the File Descriptor, and the Deployment
Two production bugs from subprocess isolation: shared database connections after fork, and lost working directories after deployment.
-
Hunting Memory Leaks in a Django Task Worker
Production memory climbing to 500 MB. The fix: run tasks in subprocesses so the OS reclaims everything. From 500 MB to 50 MB.
-
django-simple-queue: 300 Lines to Replace Celery
How a ~300 LOC task queue built on Django ORM replaces Celery for small teams — the architecture, the tradeoffs, and when it makes sense.