seL4 माइक्रोकर्नेल का परिचय [PDF]

 (sel4.systems)
1 पॉइंट द्वारा GN⁺ 2025-03-24 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • seL4 सुरक्षा और सेफ्टी-क्रिटिकल embedded तथा cyber-physical systems के लिए बनाया गया एक OS माइक्रोकर्नेल है, जो hardware resources को isolate और multiplex करता है, लेकिन यह पूर्ण general-purpose OS नहीं है
  • kernel mode code को लगभग 10 kSLOC तक घटाकर यह TCB और attack surface को कम करता है, और file system, network, driver जैसी OS services को user mode में भेज देता है
  • यह code-level formal verification वाला दुनिया का पहला OS kernel है, और सही तरह से configured system में kernel confidentiality, integrity और availability जैसी security properties तक की गारंटी देता है
  • capability-आधारित access control, WCET analysis, mixed-criticality real-time systems support, और hypervisor features को मिलाकर यह fine-grained isolation और real-time behavior दोनों को संभालता है
  • seL4 API बहुत low-level है, इसलिए complex systems को सीधे बनाना कठिन है; जहाँ static architecture उपयुक्त हो वहाँ Microkit जैसे framework का उपयोग अधिक व्यावहारिक है

seL4 का कार्यक्षेत्र

  • seL4 operating system के low-level core, यानी माइक्रोकर्नेल, के रूप में काम करता है
    • OS processor के अधिक privileged execution mode, यानी kernel mode, में hardware और resources को नियंत्रित करता है
    • applications user mode में चलती हैं और hardware तक केवल OS द्वारा अनुमति दिए गए तरीकों से ही पहुँचती हैं
  • माइक्रोकर्नेल OS का वह core है जिसमें उच्च विशेषाधिकार पर चलने वाले code को न्यूनतम रखा जाता है
    • seL4, L4 microkernel family का हिस्सा है, जिसका इतिहास 1990 के दशक के मध्य तक जाता है
    • seL4 का seLinux से कोई संबंध नहीं है
  • seL4 पूर्ण OS नहीं, बल्कि hardware resources को सुरक्षित रूप से multiplex और isolate करने वाला low-level kernel है
    • file system, network stack, device driver जैसी सामान्य OS services kernel के अंदर नहीं होतीं
    • इन services को user mode programs के रूप में उपलब्ध कराना होता है

माइक्रोकर्नेल संरचना और attack surface में कमी

  • Linux जैसे monolithic kernel file storage, networking जैसी OS services को kernel mode code के रूप में प्रदान करते हैं
    • kernel mode code को system resources तक बिना सीमा के पहुँच मिलती है, इसलिए यदि bug privilege escalation या arbitrary code execution तक पहुँच जाए तो पूरा system प्रभावित हो सकता है
    • Linux kernel का आकार लगभग 20 MSLOC है, और अनुमान है कि इसमें हजारों bugs हो सकते हैं
  • seL4 जैसे अच्छे ढंग से डिज़ाइन किए गए माइक्रोकर्नेल kernel mode code को लगभग 10 kSLOC तक सीमित कर देते हैं
    • यह Linux kernel की तुलना में कई orders of magnitude छोटा है
    • TCB कम होने से attack surface भी घटता है
  • अधिकांश OS services kernel से बाहर चली जाती हैं, और माइक्रोकर्नेल hardware के आसपास एक पतले wrapper की तरह काम करता है
    • इसका मुख्य कार्य programs के बीच isolation और सुरक्षित call mechanism देना है
    • services kernel के भीतर नहीं, बल्कि अलग sandbox में चलने वाले user mode programs बन जाती हैं
  • ज्ञात Linux compromise मामलों में गंभीर घटनाओं का विश्लेषण करने वाले एक अध्ययन के अनुसार, माइक्रोकर्नेल डिज़ाइन 29% मामलों को पूरी तरह समाप्त कर सकता था और अतिरिक्त 55% मामलों को इतना कम कर सकता था कि वे अब गंभीर श्रेणी में न आते

PPC, capability, और सूक्ष्म अधिकार नियंत्रण

  • seL4 protected procedure call (PPC) mechanism प्रदान करता है
    • ऐतिहासिक कारणों से IPC शब्द अब भी उपयोग में है, लेकिन IPC शब्द भ्रम पैदा कर सकता है और खराब डिज़ाइन की ओर ले जा सकता है
    • PPC एक program को दूसरे sandbox में मौजूद program के function को सुरक्षित रूप से call करने देता है
  • माइक्रोकर्नेल PPC में input और output को पास करता है और interface को enforce करता है
    • remote function को केवल exported entry point से ही call किया जा सकता है
    • केवल वे explicitly authorized clients, जिन्हें उचित capability मिली हो, call कर सकते हैं
  • capability ऐसा access token है जो system के किसी विशेष resource तक पहुँच देता है
    • यह बहुत सूक्ष्म स्तर पर नियंत्रित करता है कि कौन-सी entity किस resource तक पहुँच सकती है
    • यह principle of least authority, यानी POLA, का समर्थन करता है
  • Linux या Windows जैसे मुख्यधारा के systems की access control पद्धतियों से इस स्तर का least privilege हासिल नहीं किया जा सकता
  • seL4 capability-based होने के साथ formal verification वाला दुनिया का एकमात्र OS है, और इसी संयोजन के कारण इसे दुनिया का सबसे सुरक्षित OS कहने का ठोस आधार माना जाता है

formal verification और security guarantees

  • seL4 implementation correctness के लिए formal, mathematical, machine-checked proof प्रदान करता है
    • इसका अर्थ है कि specification के संदर्भ में kernel बहुत मजबूत अर्थ में “bug-free” है
    • seL4 code level पर ऐसा proof रखने वाला दुनिया का पहला OS kernel है
  • implementation correctness के अलावा seL4 security enforcement के लिए अतिरिक्त proofs भी देता है
    • सही तरीके से configured seL4-based system में kernel confidentiality, integrity और availability की गारंटी देता है
  • verification chain, seL4 की मुख्य विशेषता है
    • security और safety-critical systems में kernel को trust base बनने के लिए implementation और security properties दोनों पर मजबूत आश्वासन चाहिए

real-time behavior और mixed-criticality systems

  • seL4 ऐसा OS kernel है जिस पर worst-case execution time (WCET) का पूर्ण और sound analysis किया गया है
    • यदि kernel को सही तरह configure किया जाए, तो सभी kernel operations समय की दृष्टि से bounded होते हैं
    • और उनकी सीमा ज्ञात होती है
  • यह गुण hard real-time systems बनाने के लिए आवश्यक शर्त है
    • ऐसे systems के लिए, जहाँ बहुत सख्त समय सीमा के भीतर event का जवाब न दे पाना विनाशकारी हो सकता है
  • seL4 mixed-criticality systems (MCS) का भी समर्थन करता है
    • यह उन वातावरणों के लिए है जहाँ कम-trust code उसी platform पर साथ चलने पर भी महत्वपूर्ण activities की timing guarantees बनी रहनी चाहिए
    • पारंपरिक MCS OS द्वारा उपयोग किए जाने वाले कठोर और अलचीले time-space partitioning के विपरीत, seL4 ऐसा flexible model देता है जो resource utilization बनाए रखता है

hypervisor के रूप में seL4

  • seL4 माइक्रोकर्नेल होने के साथ-साथ hypervisor भी है
    • seL4 के ऊपर virtual machines चलाई जा सकती हैं
    • virtual machine के भीतर Linux जैसे सामान्य guest OS चलाए जा सकते हैं
  • guest और applications, seL4 द्वारा लागू communication channels के अनुसार एक-दूसरे से communicate कर सकते हैं
    • वे native applications के साथ भी communicate कर सकते हैं
  • Linux VM को system services उपलब्ध कराने के साधन के रूप में उपयोग किया जा सकता है
    • उदाहरण configuration में networking और storage जैसी services अलग VM में चलने वाले कई Linux instances से ली जाती हैं

seL4 पर system बनाने के तरीके

  • seL4 API अन्य माइक्रोकर्नेल्स की तुलना में भी बहुत low-level है
    • यह hardware को सुरक्षित रूप से प्रबंधित करने के लिए आवश्यक न्यूनतम abstractions ही देता है
    • seL4 को “operating systems की assembly language” से तुलना की जाती है
  • जटिल systems को सीधे seL4 पर बनाना उपयुक्त नहीं है
    • उच्च-स्तरीय frameworks को service implementation code पर ध्यान केंद्रित करने देना चाहिए, और hardware complexity तथा system integration को automate करना चाहिए
  • seL4 के लिए तीन प्रमुख open source component frameworks हैं
    • Microkit: protection domain-केंद्रित कम abstractions के साथ seL4 API को सरल बनाता है, और अलग compile modules तथा kernel binary को एकीकृत करके bootable image बनाने वाला SDK देता है
    • CAmkES: Microkit का पूर्ववर्ती है और static architecture systems के लिए component framework है, लेकिन SDK न होने से build process अधिक असुविधाजनक है और overhead भी अधिक है
    • Genode: कई माइक्रोकर्नेल्स को support करता है, x86 platform के लिए services और drivers समृद्ध हैं, और static architecture को अनिवार्य नहीं करता, लेकिन seL4 की सभी security और safety features का लाभ नहीं उठा पाता और इसके पास assurance story नहीं है
  • जब तक static system architecture आपकी requirements से मेल खाती है, seL4-based systems के निर्माण के लिए Microkit की सिफारिश की जाती है
    • static architecture ऐसा model है जिसमें modules के set और communication structure को system configuration के समय ही परिभाषित किया जाता है
    • माना जाता है कि यह model अधिकांश embedded systems की requirements के अनुकूल है, जिनमें automotive और aircraft जैसे जटिल cyber-physical systems भी शामिल हैं

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

1 टिप्पणियां

 
GN⁺ 2025-03-24
Hacker News की राय

  • seL4 अपने-आप में पुरानी बात है, लेकिन मैं सोच रहा हूँ कि microkernel से आगे कोई नई formally verified layers या components जोड़े गए हैं या नहीं
    साथ ही ‘proof’ शब्द देखते ही कुछ लोगों पर भावनात्मक overload आ जाता है और उनकी सोच रुक जाती है, ऐसा भी लगता है। Formal verification सुरक्षित IT जैसी अनंत समस्या का इलाज करने वाली कोई रामबाण दवा नहीं है, न ही flawless software बनाने का तरीका है
    मेरी समझ के हिसाब से यह इस बात का proof है कि कुछ खास conditions में कुछ खास requirements पूरी होती हैं, और वे requirements व conditions काफी संकीर्ण हो सकती हैं; spec के बाहर की functionality और conditions के बारे में यह कुछ नहीं कहता। क्या यह मोटे तौर पर सही है, यह जानना चाहता हूँ
    Practical तौर पर security expert ‘formally verified software’ देखकर क्या उम्मीद करते हैं, यह भी जानना चाहता हूँ। मुझे लगता है कि seL4 किस spec को satisfy करता है, यही यहाँ मुख्य जानकारी है

    • कई flaws न होने के लिए formally verified होने के बावजूद seL4 memory corruption flaws से immune नहीं था। कुछ साल पहले memory corruption flaw मिला था, और उसे ठीक करने वाला commit तथा seL4 proof को update करने वाला PR सार्वजनिक हैं
      https://github.com/seL4/seL4/pull/243
      https://github.com/seL4/l4v/pull/453
      issue tracker में भी memory से जुड़े कई bugs हैं
      https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
      दिलचस्प बात यह है कि memory के “register clobbering” को ठीक करने वाले PR पर bug label नहीं लगा, इसलिए “bug” से filter करने पर वह नहीं दिखता। पहले मैं सोचता था कि proof की वजह से seL4 ऐसे issues से immune है, लेकिन इसे देखने के बाद लगा कि proof उतना comprehensive नहीं है जितना community मानने लगी थी। फिर भी seL4 अब भी बेहद impressive software है
      सवाल का जवाब दें तो seL4 जिस spec को satisfy करता है, वह GitHub पर सार्वजनिक है
      https://github.com/seL4/l4v
    • formally verified layers या components लगातार जोड़े जा रहे हैं। हाल में RISC-V जैसी नई architectures का support, mixed-criticality scheduling, Microkit, Device Driver Framework शामिल हुए हैं
      mixed-criticality scheduling CPU time के लिए capability-based access, thread execution की upper bound limit, high-criticality tasks की priority और resource access guarantee, और caller द्वारा donate किए गए scheduling time पर चलने वाले “passive servers” देता है
      Microkit seL4 के ऊपर वास्तविक systems बनाना काफी आसान करने वाली verified abstraction layer है, और Device Driver Framework seL4 में high-performance I/O के लिए device driver templates, control/data plane implementations, driver लिखने और device virtualization के tools हैं
      Formal verification यह guarantee कर सकता है कि खास conditions में खास requirements सही रहती हैं। आम तौर पर यह बात सही है कि ऐसी requirements और conditions narrow हो सकती हैं, लेकिन seL4 खुद kernel से अपेक्षित व्यापक range की properties को cover करने वाले कई proofs रखता है, और वे guarantees बहुत कमजोर assumptions के तहत भी लागू होती हैं। C compiler की correctness भी assume नहीं की जाती; एक अलग tool है जो compiler output को देखकर prove करता है कि compiled binary मांगी गई C semantics के हिसाब से behave करती है
      seL4 जिन requirements को satisfy करता है, उनमें यह शामिल है कि seL4 kernel का binary code abstract specification में लिखे behavior को ठीक-ठीक implement करता है और उससे ज्यादा कुछ नहीं करता। buffer overflow, memory leak, pointer error, null pointer dereference, C code का undefined behavior, और spec में listed explicit तरीकों के अलावा kernel termination नहीं होते
      specification और seL4 binary integrity और confidentiality security properties भी satisfy करते हैं। integrity का मतलब है कि किसी process के पास explicit permission न हो तो वह data बदलने का कोई तरीका नहीं रखता, और confidentiality का मतलब है कि बिना permission वाले data को किसी भी तरह पढ़ा नहीं जा सकता। यह भी दिखाया जाता है कि खास side channels के जरिए indirect रूप से data infer नहीं किया जा सकता। security के अलावा expected worst-case execution time guarantees और scheduling properties भी पूरी होती हैं
    • seL4 developers कई सालों से funding shortage से जूझ रहे हैं। अधिकांश काम remotely piloted drones के लिए DARPA research था, और US military ऐसे drones बहुत चाहती है जिन्हें hack न किया जा सके
      मौजूदा काम broader adoption की ओर लक्षित LionsOS पर है: https://lionsos.org/
    • उदाहरण के लिए buffer overflow, null pointer exception, use-after-free आदि नहीं होते। ARM और RISCV64 पर binary के लिए functional correctness prove हो चुकी है, इसलिए C compiler तक पर भरोसा करने की जरूरत नहीं है। functional correctness के अलावा भी और कई proofs हैं
      https://docs.sel4.systems/projects/sel4/frequently-asked-que...
    • https://github.com/auxoncorp/ferros
      resources, hardware access, और capabilities को compile time पर track करने के लिए type-level programming का काफी उपयोग करता है। runtime पर problem ढूँढकर debug करना इतना खराब अनुभव है कि यह base kernel guarantees के कुछ हिस्से compiler side पर ऊपर उठाने की कोशिश है

  • मुझे guest monolithic kernels चलाने वाले microkernel hosts पसंद हैं, इसलिए servers seL4 को FreeBSD VM की safety layer और backup के रूप में चला रहे हैं, और उसके अंदर renderfarm, BEAM cluster, Jenkins के लिए jails इस्तेमाल कर रहे हैं
    अफसोस की बात यह है कि DragonflyBSD की threading और process-internal kernel, यानी hybrid kernel design के लिए ARM port नहीं है। सपना है कि 128-core Ampere Altra पर OpenMoonRay को ज्यादा efficiently चलाया जाए

    • servers में seL4 कैसे इस्तेमाल कर रहे हैं, इसके बारे में और detail में जानना चाहूँगा। और यह भी कि क्या यह production commercial server है
    • वह setup लंबी post के रूप में पढ़ने में काफी दिलचस्प लगेगा

  • अब लगता है कि माइक्रोकर्नेल के पक्ष-विपक्ष की बहस अपने-आप में बहुत मायने नहीं रखती। privileged services तक तेज, efficient और सुरक्षित access का एकमात्र तरीका hardware mitigations हैं, और software जो कर सकता है उसकी एक सीमा है
    यह 80286 और 80386 के अंतर जैसा है। बाद वाले ने असली multitasking के लिए hardware support जोड़ा, जो पहले वाले में नहीं था। उसके बाद hypervisor को संभव बनाने जैसे hardware-level protection mechanisms लगातार बढ़ते गए
    खासकर Apple अपने SoC में kernel, drivers और components को chip level पर protect करने और running thread व pointer इस्तेमाल करते समय permissions enforce करने वाली बहुत-सी capabilities डाल रहा है। https://support.apple.com/guide/security/operating-system-in...
    इसका मतलब यह नहीं कि OS को भेदा नहीं जा सकता, लेकिन permissions को सिर्फ software से manage करने की strategy की तुलना में यह कहीं ज्यादा effective है। ऐसी capabilities या मिलती-जुलती चीजों का इस्तेमाल करें तो kernel architecture अब उतना important नहीं लगता; सोच रहा हूं कि क्या मैं गलत हूं

    • गलत हैं। OS research के क्षेत्र में अभी भी बहुत काम बाकी है, और नए hardware के लिए software interfaces और API की जरूरत है
      ज्यादा composable micro/hybrid systems से भी सीखने को बहुत कुछ है। उदाहरण के लिए Plan 9 एक शानदार hybrid system है, जो एक single protocol 9P के जरिए system के सभी objects को user space में उपलब्ध कराता है। IP या TLS जैसी कुछ चीजें system call overhead से बचने के लिए kernel के अंदर होती हैं, इसलिए यह hybrid है
      एक और दिलचस्प design यह है कि kernel के अंदर के drivers आम तौर पर minimal रूप में होते हैं, जो hardware logic के लिए बस 9P interface जैसा काम करते हैं। इससे pointers या records जैसे machine objects को navigable files में बदला जा सकता है, standard Unix permissions से उन files को protect किया जा सकता है, और network के जरिए components को कई machines पर आसानी से distribute किया जा सकता है। नतीजतन driver logic को सुरक्षित रूप से user-space programs में धकेला जा सकता है
      9P network और architecture के लिहाज से transparent है, इसलिए Arm, x86, mips आदि कई machines पर सीधे साथ मिलकर काम किया जा सकता है। Plan 9 से Linux/Unix या Windows पर लौटना दुखद और झुंझलाहट भरा लगता है। flexibility लगभग आग्नेय चट्टान जैसी कठोर है, और वही काम—files/objects उपलब्ध कराना—करने वाले ढेरों protocols के जरिए features ऐसे जोड़ दिए गए हैं कि वे एक-दूसरे से compatible नहीं रहते
    • माइक्रोकर्नेल की उपयोगिता hardware/software co-design से अलग axis पर है
      practical engineering नजरिए से monolithic kernels ज्यादा तेज, आसान और ज्यादा संसाधनों वाले रहे हैं, और security C में जितनी संभव थी उतनी—यानी best effort और ढेर सारे bugs। उस अव्यवस्था को mitigate करने के लिए बहुत-सा hardware लाया गया। लेकिन SeL4 के साथ, process isolation और root-level exploits के न होने पर confidence बहुत ज्यादा है, इसलिए theoretically security coprocessor की जरूरत न भी पड़े। इसलिए hardware/software co-design important है
      हालांकि SeL4 team को भी hardware के side channels हटाने में काफी engineering resources लगाने पड़े। असली दुनिया physics simulation की परवाह नहीं करती, इसलिए hardware में भी flaws होते हैं
      यहां माइक्रोकर्नेल का फायदा यह है कि वह formal verification के दायरे में आने लायक छोटा होता है। proof खुद kernel size का 10 गुना है। SeL4 का context switch Linux से एक single-digit multiple तेज है, इसलिए performance impact negligible होना चाहिए। लेकिन अगर जादुई तरीके से लाखों lines वाले monolithic kernel को verify किया जा सके, तो context switch न करना अब भी ज्यादा तेज होगा। असल में SeL4 team scheduler को user space में ले जाना चाहती थी, लेकिन performance cost बहुत ज्यादा थी, इसलिए उसे kernel के अंदर ही रखा और proof burden में जोड़ा
    • पता नहीं 80286 और 80386 की तुलना अच्छी analogy है या नहीं। 286 भी protected mode में असली multitasking support करता था और कई non-DOS operating systems में इस्तेमाल हुआ। 386 ने जो चीजें जोड़ीं, उनमें से एक virtual 8086 mode था, जिसने hardware तक सीधे access करने वाले पुराने real-mode DOS applications की multitasking संभव की
    • यह explanation सही नहीं लगती। मजबूत hardware protection होने पर भी Linux का trusted computing base माइक्रोकर्नेल से कैसे comparable हो सकता है? जब तक वही protection domains फिर से reproduce न किए जाएं, Linux में ज्यादा vulnerabilities बची रहेंगी
      बल्कि hardware की मुख्य भूमिका efficiency बढ़ाना है। उदाहरण के लिए आज के माइक्रोकर्नेल पहले से ही MMU जैसे hardware का अच्छा उपयोग करते हैं, इसलिए वे काफी robust हैं। फिर माइक्रोकर्नेल का छोटा trusted computing base kernel को reliability देता है, और kernel व hardware मिलकर एक मजबूत foundation बनाते हैं
      आखिरकार बात यह है कि hardware से किस हद तक “cheating” की अनुमति दी जाए, लेकिन overall माइक्रोकर्नेल protection features का बेहतर इस्तेमाल करता है। या फिर exokernel को भी देखा जा सकता है

  • https://genode.org/index
    यह seL4 support वाला operating system है

    • सोच रहा हूं कि Genode के कोई उल्लेखनीय use cases हैं या नहीं

  • स्थानीय OWASP चैप्टर में मैंने कभी SeL4 पर प्रेज़ेंटेशन दिया था। पता नहीं सामग्री ढूंढ पाऊंगा या नहीं
    यह प्रोजेक्ट वाकई बहुत अच्छी तरह बना है, लेकिन खासकर general-purpose computing में इसे Linux का विकल्प मानने में झिझक होती है। इसका मतलब यह नहीं कि microkernel आम तौर पर general-purpose उपयोग के लिए खराब हैं। RedoxOS ने हाल में कुछ प्रगति की लगती है और यह Rust में लिखे microkernel का उपयोग करता है

    • समस्या हमेशा यह होती है कि “आप कितने बड़े दायरे के replacement की बात कर रहे हैं”। Redox लगता है POSIX interoperability को अच्छी तरह बनाए रखना चाहता है, और यह स्वाभाविक रूप से design decisions को प्रभावित करता है। तकनीकी क्षमता होना और सफल होना—इन दोनों के बीच भी बड़ा अंतर है
      फिर भी अगर Redox सफल होता है, तो वह अपने आप में अच्छी प्रगति होगी। seL4 में ये विशेषताएं और भी चरम रूप में हैं। तकनीकी फायदे बेहतरीन हैं, लेकिन अब तक भी और शायद आगे भी, इसमें ‘अगली बड़ी चीज़’ बनने के लिए जरूरी कुछ नहीं होगा। राजनीतिक पहलुओं को अलग रखें तो मेरा मानना है कि microkernel सफल होंगे, और उन्हें होना भी चाहिए
    • Linux को replace कर पाने की संभावना scenario पर निर्भर करती है। बेशक Linux संभालना आसान है, लेकिन उल्टा ऐसी requirements भी हैं जिन्हें केवल seL4 ही पूरा कर सकता है
      seL4 को सच में उपयोगी बनाने के लिए उसके ऊपर बहुत कुछ चाहिए। अच्छी बात है कि उस हिस्से में भी काफी open source काम हुआ है, और यह कुछ साल पहले की तुलना में कहीं बेहतर स्थिति में है
      static scenarios के लिए LionsOS[0] है और यह पहले से काफी usable है
      dynamic scenarios के लिए Provably Secure, General-Purpose Operating System[1] है, लेकिन वह अभी शुरुआती चरण में है
      दोनों seL4 वेबसाइट से linked trustworthy systems के Projects page[2] पर मिल सकते हैं
      [0] https://trustworthy.systems/projects/LionsOS/
      [1] https://trustworthy.systems/projects/smos/
      [2] https://trustworthy.systems/projects/

  • मुझे जिज्ञासा है कि इस kernel के ऊपर चलने वाले OS को भी security guarantees मान्य रहने के लिए formally verified होना जरूरी है या नहीं

    • kernel जो guarantees देता है, उन्हें उसके ऊपर चलने वाले unprivileged processes तोड़ नहीं सकते
      बेशक सिर्फ kernel अपने आप में बहुत उपयोगी नहीं होता, इसलिए kernel के ऊपर चलने वाले drivers, filesystem servers और अन्य services का design अभी भी महत्वपूर्ण है
      यह भी महत्वपूर्ण है कि Linux सहित अधिकतर दूसरे systems बुनियादी स्तर पर flawed हैं, लेकिन seL4 वास्तव में secure और trustworthy systems बनाना संभव करता है
    • नहीं। फायदा यह है कि kernel isolation की guarantee देता है, इसलिए kernel और processes पर भरोसा करने की जरूरत नहीं होती
      इसलिए आप high-security process के बगल में Linux kernel चला सकते हैं, और allowed IPC को छोड़कर, उनके एक-दूसरे से isolated रहने की guarantee रख सकते हैं
    • नहीं
      लेकिन limitations हैं। DMA बंद करना होगा, और drivers भी केवल formally verified वाले ही इस्तेमाल करने होंगे
      यह भी महत्वपूर्ण है कि seL4 का multicore kernel अभी verified नहीं है
    • absolute sense में देखें तो हां कहा जा सकता है। practical level पर paper के section 7.2 में आंशिक जवाब मिल सकता है

  • Drew DeVault का Helios Microkernel भी देखने लायक है। कहा जाता है कि यह SeL4-based है
    https://ares-os.org/docs/helios/

    • “based on” और “inspired by” के बीच meaningful फर्क होता है, और Helios बाद वाले के ज्यादा करीब लगता है

  • Karlsruhe यूनिवर्सिटी में L4 लोकप्रिय था। मैंने इसे गहराई से कभी नहीं देखा, लेकिन यह ऐसा प्रोजेक्ट लगता था जिसकी रुचि व्यावहारिक रूप से उपयोगी चीज़ बनाने के बजाय मुख्य रूप से सैद्धांतिक ideas को परखने में थी
    वह 20 साल पहले की बात थी, और मुझे लगता है कि आज भी इसमें बहुत बदलाव नहीं आया है। जल्दी से खोजने पर लगता है कि इसके ऊपर OS बनाने की कोशिशें हुई हैं, लेकिन वे वास्तविक उपयोग से ज़्यादा proof of concept जैसी दिखती हैं

    • https://en.wikipedia.org/wiki/L4_microkernel_family देखने पर पता चलता है कि L4 कई जगहों पर इस्तेमाल हुआ है, और लगता है कि मुख्य रूप से embedded environments में इस्तेमाल किया गया
      “OKL4 की shipments 2012 की शुरुआत में 1.5 अरब से ज़्यादा हो गई थीं, जिनमें ज़्यादातर Qualcomm wireless modem chips थे। अन्य deployments में automotive infotainment systems शामिल हैं”
      “A7 से शुरू होने वाले Apple A-series processors में Secure Enclave coprocessor होता है जो L4 operating system चलाता है, और यह OS 2006 में NICTA द्वारा विकसित L4-embedded kernel पर आधारित sepOS है। नतीजतन L4, Apple silicon वाले Macs सहित, सभी आधुनिक Apple devices में मौजूद है”
    • Jochen Liedtke 1999 में Karlsruhe में professor बने, लेकिन दुर्भाग्य से 2001 में कुछ ही समय बाद उनका निधन हो गया। मुझे नहीं पता कि उनके उत्तराधिकारी Bellosa अभी भी L4 research कर रहे हैं या नहीं। L4Ka project था, लेकिन लगता है कि वह पूरा हो चुका है। Bellosa के undergraduate operating systems lecture में यह curriculum में शामिल नहीं है
      Bellosa के alumnus Rittinghaus Unikraft[0] से जुड़े हैं, जिसे HN पर भी कई बार पेश किया गया है, और यह unikernel technology का उपयोग करता है
      [0] https://unikraft.org/
    • iPhone में L4 variant इस्तेमाल होता है
      “Secure Enclave Processor, Apple द्वारा customized L4 microkernel का version चलाता है”
      https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
    • open source derivative L4Re सभी id.X Volkswagen vehicles के central “icas1” ECU पर चलता है, और Linux तथा अन्य guests को host करता है
      https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
      मुझे लगता है कि L4Re kernel भी Elektrobit Safe Linux का हिस्सा है
    • Karlsruhe team ने L4Ka, खासकर Pistachio में जो काम और दिशा ली, वह मुझे पसंद है। design साफ़-सुथरा, सरल और समझने में आसान था
      मैंने अपनी graduation thesis के रूप में Pistachio-आधारित OS बनाया था। मैंने हमेशा सोचा कि अगर मैंने Karlsruhe में पढ़ाई की होती, तो शायद OS research में गया होता

  • मेरे पास भी operating system design के ideas थे, और जिस capability पर मैंने विचार किया था, उसमें seL4 जैसी interposition और delegation features इस्तेमाल होते थे। वहां लिखी बातों के अलावा भी इसके फायदे हैं। उदाहरण के लिए, audio पर filters लगाने या network transparency implement करने के लिए proxy capability इस्तेमाल की जा सकती है
    मुझे लगता था कि real-time features को optional implementation के रूप में अनुमति दी जा सकती है। मेरा idea एक single implementation नहीं, बल्कि specification के ज्यादा करीब था
    एक और feature जो मैं चाहता था वह यह था कि सभी programs input/output को छोड़कर deterministically behave करें। input/output के बिना date/time या program execution time पता नहीं चल सकता, और processor features भी check नहीं किए जा सकते। अगर कोई ऐसी feature इस्तेमाल की जाए जिसे hardware support नहीं करता, तो operating system उसे emulate कर सकता है
    इसे implement करने के लिए मैं hardware support और software support का मिश्रण इस्तेमाल करने की सोच रहा था। document में hardware-implemented capability पर attacks के notes हैं, लेकिन मेरे पास reference documents नहीं हैं, इसलिए नहीं पता कि वे attacks उस तरीके पर भी लागू होते हैं या नहीं जिसकी मैं कल्पना कर रहा था

  • security के नजरिए से, यह Linux kernel के KVM जैसी failure दिखाता है। अगर hypervisor ring 0 में हो, तो एक VM से दूसरे VM या host itself में escape करने का जोखिम होता है
    मुझे उत्सुकता है कि इस risk को कैसे mitigate किया जाता है

    • seL4 के virtualization support में VM exceptions messages में बदल जाते हैं, और इन्हें VMM handle करता है, जो unprivileged mode में चलने वाला task है
      VMM के पास VM itself से ज़्यादा capabilities नहीं होतीं, इसलिए academic अर्थ को छोड़ दें तो VM escape की कोई value नहीं है
      original PDF के pages 8–10 देखें