Ironclad – रीयल-टाइम सपोर्ट वाला Unix-परिवार OS कर्नेल

 (ironclad-os.org)
1 पॉइंट द्वारा GN⁺ 2025-11-10 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Ironclad सामान्य उपयोग और एम्बेडेड परिवेशों के लिए औपचारिक सत्यापन-आधारित रीयल-टाइम सपोर्ट वाला Unix-परिवार कर्नेल है
    • औपचारिक सत्यापन(Formal verification) : रनटाइम त्रुटियों का अभाव(AoRTE, Absence of Runtime Errors) और घटकों की शुद्धता सुनिश्चित करने के लिए कर्नेल कोड पर लागू प्रक्रियाओं और जांचों की एक श्रृंखला
  • यह SPARK और Ada में लिखा गया है, और 100% मुक्त सॉफ़्टवेयर से बना है
  • POSIX-संगत इंटरफ़ेस, प्रीएम्प्टिव मल्टीटास्किंग, अनिवार्य अभिगम नियंत्रण(MAC), हार्ड रीयल-टाइम शेड्यूलिंग का समर्थन
  • GPLv3 लाइसेंस के तहत वितरित, और firmware blob के बिना पूरी तरह ओपन सोर्स संरचना बनाए रखता है
  • कई प्लेटफ़ॉर्म पर पोर्ट किया जा सकता है, और Gloire जैसी distributions के माध्यम से इसका ecosystem विस्तार कर रहा है

Ironclad ऑपरेटिंग सिस्टम कर्नेल का अवलोकन

  • Ironclad एक रीयल-टाइम सपोर्ट वाला UNIX-परिवार कर्नेल है जिसमें औपचारिक सत्यापन(formal verification) आंशिक रूप से लागू किया गया है
    • इसे सामान्य प्रयोजन और एम्बेडेड सिस्टम, दोनों को ध्यान में रखकर डिज़ाइन किया गया है
    • औपचारिक सत्यापन(Formal verification) : रनटाइम त्रुटियों का अभाव(AoRTE, Absence of Runtime Errors) और घटकों की शुद्धता सुनिश्चित करने के लिए कर्नेल कोड पर लागू प्रक्रियाओं और जांचों की एक श्रृंखला
    • इसके लिए Ada के subset SPARK का उपयोग किया जाता है
    • पूरा कोड मुक्त सॉफ़्टवेयर से बना है
  • कर्नेल POSIX-संगत इंटरफ़ेस प्रदान करता है, और प्रीएम्प्टिव मल्टीटास्किंग, अनिवार्य अभिगम नियंत्रण(MAC), हार्ड रीयल-टाइम शेड्यूलिंग का समर्थन करता है
    • यह पारंपरिक UNIX परिवेश जैसा विकास अनुभव देता है
    • रीयल-टाइम नियंत्रण की आवश्यकता वाले सिस्टम के लिए उपयुक्त संरचना

मुक्त सॉफ़्टवेयर के रूप में विशेषताएँ

  • Ironclad को GPLv3 लाइसेंस के तहत पूरी तरह ओपन सोर्स के रूप में वितरित किया जाता है
    • कर्नेल में firmware blob शामिल नहीं है
    • स्टैक के सभी घटक ओपन सोर्स रूप में उपलब्ध हैं

औपचारिक सत्यापन(Formal Verification)

  • SPARK भाषा की औपचारिक सत्यापन क्षमताओं का उपयोग करके प्रमुख घटकों में त्रुटियों की अनुपस्थिति और शुद्धता सुनिश्चित की जाती है
  • SPARK, Ada कोड में पूर्व शर्त(Pre), पश्च शर्त(Post), निर्भरता(Depends) आदि निर्दिष्ट कर कोड की तार्किक संगति का गणितीय सत्यापन करता है
    • सत्यापन के दायरे में क्रिप्टोग्राफी मॉड्यूल, MAC सिस्टम, यूज़र इंटरफ़ेस से संबंधित फ़ीचर आदि शामिल हैं

पोर्टेबिलिटी और विकास परिवेश

  • Ironclad को कई प्लेटफ़ॉर्म और बोर्ड पर पोर्ट किया गया है, और इसे इस तरह डिज़ाइन किया गया है कि अतिरिक्त पोर्टिंग आसान हो
    • केवल GNU toolchain पर निर्भर होने के कारण आसान cross-compilation संभव है
    • POSIX संगतता की वजह से सॉफ़्टवेयर पोर्टिंग और विकास आसान है

distributions और ecosystem

  • Ironclad प्रोजेक्ट विभिन्न आर्किटेक्चर और बोर्डों के लिए distribution प्रदान करता है
    • इसका एक प्रमुख मुक्त ओपन सोर्स distribution है Gloire
    • डाउनलोड के लिए tarball फ़ॉर्मेट की distribution images उपलब्ध हैं

प्रोजेक्ट समर्थन और निरंतरता

  • Ironclad एक ऐसा प्रोजेक्ट है जिसे उपयोग, शोध और संशोधन के लिए स्वतंत्र रखा गया है
    • प्रोजेक्ट का संचालन दान और अनुदान पर निर्भर है
    • हर योगदान प्रोजेक्ट के विस्तार और विकास पर सीधे प्रभाव डालता है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2025-11-10
Hacker News राय

  • यह एक दिलचस्प प्रोजेक्ट है। worst-case execution time (WCET) के formal verification की सीमाएँ क्या हैं, यह जानने की उत्सुकता है
    seL4, atmosphere जैसे दूसरे verified kernels भी हैं, और genode की तरह POSIX compatibility layer भी ऊपर जोड़ी जा सकती है
    QNX या VxWorks जैसे पूरी तरह compatible और mature kernels भी मौजूद हैं, इसलिए complete verification अपने-आप में बहुत बड़ा अतिरिक्त मूल्य न भी हो सकता है
    लेकिन WCET + formal verification + POSIX compatibility—ये तीनों एक साथ बहुत कम देखने को मिलते हैं
    अभी के चरण पर यह कहना मुश्किल है कि इसकी maturity इतनी है कि documentation में बताए गए real-time use cases में इसे सीधे इस्तेमाल किया जा सके

    • अब दुनिया ऐसी है कि कोई भी सरकार किसी OS पर RCE हासिल कर सकती है। इसलिए process isolation का formal verification सच में बहुत महत्वपूर्ण है
      seL4 Linux से काफी तेज है, लेकिन यह शायद धीमा होगा। POSIX में बुनियादी खामियाँ हैं, और MAC इतना जटिल है कि व्यवहारिक काम में इस्तेमाल करना मुश्किल होता है
    • अभी यह stone स्तर पर है, लेकिन आगे चलकर इसे official certification भी मिल सकती है। formally verified OS सुरक्षा सुधार की दिशा में बड़ा कदम है

  • Ada, Wirth family languages (Pascal family) में आती है। अब तक Wirth family language में बना Unix-जैसा kernel मुझे सिर्फ TUNIS ही पता था
    TUNIS को Concurrent Euclid में implement किया गया था

    • 90 के दशक में University of Washington का SPIN भी था। यह Modula-3 में लिखा एक microkernel-based system था, जो Digital UNIX system call interface को support करता था
      इसी तरह 80 के दशक में INRIA का Sol Pascal dialect में implement किया गया था और Unix-compatible environment देता था, जिसके बाद Chorus आया

  • Ironclad नाम की एक NDA-संबंधित कंपनी भी है। trademark समस्या से सावधान रहना चाहिए
    फिर भी ऐसी कोशिशें देखना सच में अच्छा लगता है। लेकिन व्यवहारिक दुनिया में security की सबसे कमजोर कड़ी firmware layer होती है
    मेरा सपना है कि Framework Computer जैसे hardware में verified EFI firmware हो और हर component के firmware का audit किया गया हो

    • Ironclad, Common Lisp की एक प्रमुख cryptography library का नाम भी है (ironclad GitHub)
    • MNT Research भी देखने लायक है। यह repairable laptops बनाती है और hardware व software दोनों को open source करती है (mnt.re)
    • firmware verification के लिए अलग kernel चाहिए। अब तो ऐसे हिस्सों को regulatory level पर संभाला जाना चाहिए
    • trademark में, एक ही नाम होने पर भी अलग industry domain हो तो समस्या नहीं होती। जैसे Apple Computer और Beatles के Apple Music का मामला (xkcd 386)

  • नया OS बनाना सच में ambitious काम है। हाल ही में Radiant Computer भी आया था; सोच रहा हूँ, क्या ऐसे और भी रोचक प्रोजेक्ट हैं

    • Asterinas (Linux-compatible kernel) और Redox OS आशाजनक हैं
    • SerenityOS भी है
    • पुराना विकल्प होने के बावजूद Haiku OS अब भी दिलचस्प है
    • मेरे पास भी OS के कुछ विचार हैं। hardware, kernel, और user programs तक शामिल कई components के बारे में सोच रहा हूँ
    • ReactOS भी लगातार आगे बढ़ रहा है। यह पूरी तरह नया OS नहीं है, लेकिन फिर भी मुझे नया लगता है

  • उम्मीद है कि कभी fully formally verified kernels आम हो जाएंगे
    पूरे Linux का verification करना शायद असंभव है, लेकिन seL4 को smartphone जैसे बाजारों में मौका मिल सकता है

    • seL4 का इस्तेमाल पहले से Secure Enclave OS आदि में हो रहा है (L4 microkernel family)
    • seL4 पहले से कई जगह इस्तेमाल हो रहा है, और use cases तथा member companies list देखें तो आगे इसके और फैलने की संभावना दिखती है

  • उनका verification roadmap देखें तो इसे “formal verification” कहना कुछ ज़्यादा लगता है
    kernel की मुख्य properties के proofs नहीं हैं, और यह seL4 या Tock जैसे kernels के स्तर तक नहीं पहुँचता

  • CuBit, SPARK/Ada में लिखा एक और OS है
    इसका source GitHub पर देखा जा सकता है

  • आम उपयोगकर्ता के नज़रिए से सिर्फ kernel अपने-आप में उपयोगी नहीं है
    Ironclad kernel का उपयोग करने वाले OS का एक उदाहरण Gloire है

  • MAC पर documentation अच्छी तरह व्यवस्थित है (Mandatory Access Control)

  • SPARK में “contact us for pricing” लिखा है, तो यह ‘free software’ वाले अर्थ में free नहीं, शायद किसी और अर्थ में free है

    • ऊपर दिए गए GitHub links में भी commercial support आम तौर पर paid है। pricing पूछना सामान्य प्रक्रिया है, इसमें कुछ खास अजीब नहीं है
    • आखिर developers को भी रोज़ी-रोटी कमानी होती है, और यह बिल्कुल स्वाभाविक है