C bounded model checker: अपराधवश कम उपयोग किया गया
CBMC, C के लिए एक bounded model checker (और Rust के लिए Amazon के Kani का backend), को सीमाओं के भीतर program paths का exhaustively exploration करके buffer overflows और logic errors जैसे सूक्ष्म bugs पकड़ने के लिए सराहा जाता है। टिप्पणीकार इस पर बहस करते हैं कि ये tools छोटे, unit-test-जैसे code से आगे कितनी अच्छी तरह scale करते हैं, Frama-C, KLEE और sanitizers जैसे विकल्पों की तुलना में कैसे हैं, और क्या इन्हें अपनाने में लगने वाला प्रयास safer languages पर स्विच करने से बेहतर है। बातचीत C की पुरानी समस्याओं—undefined behavior, array-length information की कमी, और कमजोर safety guarantees—तक फैल जाती है, और यह कि language evolution या external tools low-level software को सुरक्षित बनाने का अधिक यथार्थवादी रास्ता हैं या नहीं।
CBMC का अपनाना और उपयोग के मामले
- कई टिप्पणीकारों का तर्क है कि CBMC का कम उपयोग हो रहा है और वे हार्डवेयर-शैली की formal verification को मुख्यधारा के software में लाने की वकालत करते हैं।
- उद्धृत उदाहरण: crypto code, AWS C libraries, FreeRTOS components, HTTP client functions, और बड़े commercial C projects (~500K LOC) का verification।
- कुछ users ने वास्तविक bugs पाए होने की रिपोर्ट दी, जैसे buffer overflows, denial-of-service loops, और parsers तथा networking code में समस्याएँ।
Scalability और Verification Style
- आम सहमति: CBMC unit या छोटे-module स्तर पर सबसे अच्छा काम करता है, पूरे बड़े systems पर नहीं।
- प्रभावी उपयोग के लिए आवश्यक है:
- Contract-based design: स्पष्ट pre/postconditions और assertions।
- “Shadow” functions जो जटिल callees को सरल, nondeterministic models से बदल देती हैं, जो वही contract सम्मान करें।
- Search depth को shallow रखना ताकि हर run जल्दी पूरा हो।
- Legacy, खराब संरचित code पर retrofit करना, इसे शुरुआत से उपयोग करने की तुलना में अधिक कठिन माना जाता है।
अन्य Tools से तुलना
- Frama-C, Coq VST, seL4 का approach: अधिक शक्तिशाली, लेकिन अधिक expertise की आवश्यकता और रोज़मर्रा के code पर आसानी से scale नहीं करते।
- KLEE: GNU text/coreutils जैसे सरल tools पर अच्छा; complex structured inputs (जैसे protobufs, C++ containers) पर संघर्ष करता है।
- Static analyzers (जैसे compiler analyzers plus annotations) कुछ buffer issues को कवर कर सकते हैं; CBMC को फिर भी एक और safety layer के रूप में महत्व दिया जाता है।
- CBMC का उपयोग Kani के backend के रूप में भी होता है, जो Rust verification tool है।
C Arrays, Bounds, और Language Design
- C में array का size pointer में decay होने पर खो जाने और उसके परिणामस्वरूप buffer bugs पर विस्तृत बहस हुई।
- चर्चा किए गए प्रस्ताव: fat pointers/slices, non-owning sized arrays, और pointer-to-array parameters; कुछ अन्य languages में लागू हैं।
- निराशा कि C standards ने ऐसे features नहीं अपनाए, जबकि Unicode identifiers जैसी अधिक obscure चीज़ें जोड़ दी गईं।
Undefined Behavior और Uninitialized Memory
- CBMC uninitialized locals को nondeterministic values के रूप में model करता है, जो C की UB semantics से अलग हो सकता है।
- कुछ लोग तर्क देते हैं कि verifier को किसी भी UB (जैसे uninitialized variables पढ़ना) को तुरंत error मानना चाहिए; अन्य लोग नोट करते हैं कि CBMC का वर्तमान focus exact C semantics नहीं, बल्कि “C-like” models है।
- UB, compiler optimizations, “friendly/boring C,” sanitizers, और OS behavior पर लंबे subthread में UB-driven miscompilations और security bugs को लेकर गहरी चिंता दिखाई गई।
- इस बात पर सहमति है कि CBMC को compiler warnings और sanitizers के साथ defense in depth के हिस्से के रूप में उपयोग किया जाना चाहिए.