💻 computer science

Misquoted No More: Securely Extracting F* Programs with IO

यह शोध पत्र SEIO* प्रस्तुत करता है, जो एक ऐसा ढांचा है जो रिलेशनल कोटेशन को सत्यापित सिंटैक्स जनरेशन के साथ जोड़ता है ताकि IO और रिफाइनमेंट टाइप्स वाले शैलोली एम्बेडेड F* प्रोग्राम्स को डीपली एम्बेडेड कैलकुलस में सुरक्षित रूप से निकाला जा सके, जिससे मनमाने प्रतिकूल लिंकिंग (adversarial linking) के विरुद्ध सुरक्षा सुनिश्चित करने के लिए रोबस्ट रिलेशनल हाइपरप्रॉपर्टी प्रिजर्वेशन (RrHP) के मशीन-चेक्ड प्रमाण प्रदान किए जा सकें।

मूल लेखक: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

प्रकाशित 2026-07-20

📖 8 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

अदृश्य सुरक्षा जाल (The Invisible Safety Net)

कल्पना कीजिए कि आप एक मास्टर आर्किटेक्ट हैं जिन्होंने एक शानदार, सेल्फ-ड्राइविंग कार डिजाइन की है, जो एक ऐसे आदर्श, काल्पनिक दुनिया में है जहाँ भौतिकी (physics) हमेशा ठीक वैसे ही व्यवहार करती है जैसा आप भविष्यवाणी करते हैं। आपने इसके ब्लूप्रिंट एक विशेष, अत्यंत सटीक भाषा में लिखे हैं जो गणितीय रूप से यह सिद्ध कर सकती है कि कार कभी दुर्घटनाग्रस्त नहीं होगी, कभी गलत समय पर ब्रेक नहीं मारेगी, और हमेशा सड़क के नियमों का पालन करेगी। कंप्यूटर वैज्ञानिक इसे "फॉर्मल वेरिफिकेशन" (formal verification) कहते हैं। यह एक ऐसे सपने में कार बनाने जैसा है जहाँ आप हर बोल्ट और तार के बारे में 100% सुनिश्चित हो सकते हैं।

लेकिन यहाँ एक पेंच है: वह सपनों वाली दुनिया वास्तविक सड़क पर मौजूद नहीं है। कार को वास्तव में चलाने के लिए, आपको अपने आदर्श ब्लूप्रिंट को एक ऐसी भाषा में अनुवादित करना होगा जिसे वास्तविक इंजन और टायर समझते हों, जैसे कि C या OCaml। इस अनुवाद प्रक्रिया को "एक्सट्रैक्शन" (extraction) कहा जाता है। समस्या यह है कि अनुवादक (वह कंप्यूटर प्रोग्राम जो रूपांतरण करता है) दोषरहित नहीं होता। वह एक बोल्ट गिरा सकता है, एक तार को मरोड़ सकता है, या किसी नियम को गलत समझ सकता है। यदि वास्तविक दुनिया की कार अनुवाद के दौरान हुई किसी गलती पर आधारित है, तो आपकी सुरक्षा का पूर्ण प्रमाण बेकार हो जाता है। कार कागज पर सुरक्षित दिख सकती है लेकिन वास्तविकता में दुर्घटनाग्रस्त हो सकती है।

वर्षों से, वैज्ञानिक काम के बाद अनुवादक के काम की जाँच करने के लिए प्रयास कर रहे हैं, जो कि कार बनने के बाद एक मैकेनिक द्वारा निरीक्षण करने जैसा है कि क्या वह योजनाओं से मेल खाती है। लेकिन यह शोध पत्र एक स्मार्ट तरीका पेश करता है: केवल तैयार कार की जाँच करने के बजाय, वे अनुवाद के दौरान एक "सुरक्षा प्रमाणपत्र" (safety certificate) बनाते हैं जो गणितीय रूप से यह सिद्ध करता है कि वास्तविक कार, सपनों वाली कार की एक पूर्ण जुड़वा (perfect twin) है, भले ही अनुवादक कोई गलती कर दे। वे इसे "सिक्योर एक्सट्रैक्शन" (secure extraction) फ्रेमवर्क कहते हैं, और इसे आपके डिजिटल निर्माणों को बाहरी दुनिया के अनवेरिफाइड (unverified) कोड के साथ मिश्रित होने पर भी सुरक्षित रखने के लिए डिज़ाइन किया गया है।

शोध पत्र का मुख्य विचार: "रिलेशनल कोटेशन" (Relational Quotation) का जादू

इस शोध पत्र के लेखक, जो कंप्यूटर वैज्ञानिकों की एक टीम है, ने SEIO★ (Secure Extraction of IO-star) नामक एक नया फ्रेमवर्क बनाया है। उनका लक्ष्य F★ में लिखे गए प्रोग्रामों के लिए "अनुवाद की समस्या" को हल करना था, जो क्रिप्टोग्राफिक टूल्स जैसे अत्यधिक सुरक्षित सॉफ्टवेयर लिखने के लिए उपयोग की जाने वाली भाषा है। F★ प्रोग्राम अक्सर "शैलोली एम्बेडेड" (shallowly embedded) होते हैं, जो एक फैंसी तरीका है यह कहने का कि वे एक उच्च-स्तरीय, अमूर्त (abstract) शैली में लिखे जाते हैं जो चीजें सिद्ध करने के लिए तो बेहतरीन है लेकिन कंप्यूटर के लिए वास्तविक कोड में बदलना कठिन है।

आमतौर पर, जब आप इन अमूर्त प्रोग्रामों को वास्तविक कोड में बदलते हैं, तो आपको एक "मेटाप्रोग्राम" (एक प्रोग्राम जो अन्य प्रोग्राम लिखता है) का उपयोग करना पड़ता है जो भारी काम करता है। यह करने का पुराना तरीका जोखिम भरा था: मेटाप्रोग्राम नया कोड लिखता था और फिर यह सिद्ध करने का प्रयास करता था कि नया कोड सही है। यदि प्रमाण विफल हो जाता, तो आपको फिर से शुरू करना पड़ता। यदि प्रमाण सफल हो जाता, तो भी आपको इस बात पर भरोसा करना पड़ता था कि मेटाप्रोग्राम ने प्रमाण लिखते समय कोई बग तो नहीं डाल दिया। यह एक छात्र से अपना होमवर्क खुद ग्रेड करने के लिए कहने जैसा था और यह उम्मीद करने जैसा था कि उसने नकल नहीं की होगी।

लेखकों की सफलता एक तकनीक है जिसे वे रिलेशनल कोटेशन (Relational Quotation) कहते हैं। मेटाप्रोग्राम से अंतिम कोड और प्रमाण दोनों लिखने के लिए कहने के बजाय, वे उससे कुछ बहुत सरल करने के लिए कहते हैं: एक टाइपिंग डेरिवेशन (typing derivation) लिखना। इसे एक चरण-दर-चरण रेसिपी कार्ड के रूप में सोचें जो कहता है, "चरण 1: इस सामग्री को लें। चरण 2: इसे उस सामग्री के साथ मिलाएं।" यह रेसिपी कार्ड वास्तव में भोजन नहीं बनाता है; यह केवल यह सिद्ध करता है कि सामग्रियों को एक विशिष्ट व्यंजन में पकाया जा सकता है।

यहाँ चतुर हिस्सा है:

मेटाप्रोग्राम (रेसिपी लेखक): अनवेरिफाइड मेटाप्रोग्राम मूल अमूर्त प्रोग्राम को देखता है और इस "रेसिपी कार्ड" (टाइपिंग डेरिवेशन) को उत्पन्न करता है। क्योंकि रेसिपी कार्ड मूल प्रोग्राम की सटीक संरचना का पालन करता है, इसलिए इसे लिखना बहुत आसान है।
जाँच (निरीक्षक): F★ भाषा स्वयं इस रेसिपी कार्ड की जाँच करती है। वह पूछती है, "क्या यह रेसिपी वास्तव में मूल प्रोग्राम का वर्णन करती है?" यदि मेटाप्रोग्राम ने गलती की और केक के लिए रेसिपी लिख दी जबकि मूल चीज़ सूप थी, तो जाँच विफल हो जाएगी। लेकिन यदि रेसिपी मेल खाती है, तो F★ भाषा 100% सुनिश्चित होती है कि रेसिपी वैध है।
सत्यापित चरण (मास्टर शेफ): एक बार जब रेसिपी कार्ड सत्यापित हो जाता है, तो एक अलग, पूरी तरह से सत्यापित फ़ंक्शन (एक "मास्टर शेफ" जो गणितीय रूप से पूर्ण सिद्ध किया गया है) उस रेसिपी को लेता है और अंतिम व्यंजन (वास्तविक कोड) पकाता है। क्योंकि रेसिपी को सिद्ध किया गया है कि वह मूल से मेल खाती है, और शेफ को सिद्ध किया गया है कि वह बिल्कुल वही पकाता है जो रेसिपी कहती है, इसलिए अंतिम व्यंजन की गारंटी है कि वह मूल का एक पूर्ण जुड़वा है।

यह दृष्टिकोण उस "भरोसे" को कम करता है जो हमें अनवेरिफाइड मेटाप्रोग्राम पर रखना पड़ता है। हम केवल उसे रेसिपी लिखने के लिए विश्वास करते हैं, भोजन पकाने या होमवर्क ग्रेड करने के लिए नहीं। कठिन काम—भोजन सुरक्षित है यह सिद्ध करना—एक सत्यापित मास्टर शेफ द्वारा किया जाता है।

"सिक्योर कंपाइलेशन" (Secure Compilation) की महाशक्ति

शोध पत्र केवल यह सुनिश्चित करने तक ही नहीं रुकता कि कोड सही है; यह एक कदम आगे बढ़कर यह सुनिश्चित करता है कि यह सुरक्षित है। वास्तविक दुनिया में, आपका वेरिफाइड प्रोग्राम अन्य कोड के साथ लिंक हो सकता है जो वेरिफाइड नहीं है—शायद किसी हैकर द्वारा लिखा गया कोड, या किसी दूसरी टीम द्वारा लिखा गया ढीला-ढाला कोड। यह "एडवर्सरियल" (adversarial) कोड आपके प्रोग्राम के नियमों को तोड़ने की कोशिश करता है।

लेखक उनके फ्रेमवर्क के लिए एक अत्यंत मजबूत सुरक्षा नियम को संतुष्ट करने का प्रमाण देते हैं जिसे Robust Relational Hyperproperty Preservation (RrHP) कहा जाता है। इसे समझने के लिए, कल्पना करें कि आपका वेरिफाइड प्रोग्राम एक किला है।

पुराने तरीके शायद यह कहेंगे, "किले की दीवारें मजबूत हैं, इसलिए यह सुरक्षित है।"
यह शोध पत्र कहता है, "भले ही कोई हैकर पिछले दरवाजे से घुसने की कोशिश करे, या वे गार्डों को धोखा देने की कोशिश करें, या वे खेल के नियम बदलने की कोशिश करें, आपका किला फिर भी ठीक वैसा ही व्यवहार करेगा जैसा आपने डिजाइन किया था।"

वे इसे दो "लॉजिकल रिलेशंस" (logical relations) का उपयोग करके सिद्ध करते हैं, जो दो-तरफा दर्पणों की तरह हैं। एक दर्पण यह जाँचता है कि वास्तविक कोड वह सब कुछ कर सकता है जो अमूर्त कोड कर सकता था। दूसरा दर्पण यह जाँचता है कि वास्तविक कोड वह कुछ भी नहीं करता जो अमूर्त कोड नहीं कर सकता था। दोनों को सिद्ध करके, वे दिखाते हैं कि वास्तविक कोड मूल का एक पूर्ण, सुरक्षित साया है, चाहे वह किसी भी अव्यवस्थित कोड के साथ लिंक क्यों न हो जाए।

उन्होंने वास्तव में क्या किया (और क्या नहीं किया)

टीम ने इस फ्रेमवर्क को पूरी तरह से F★ भाषा के भीतर बनाया और हर एक चरण को जाँचने के लिए एक कंप्यूटर का उपयोग किया। उन्होंने केवल अनुमान नहीं लगाया या सिमुलेशन नहीं किया; उन्होंने इसे गणितीय रूप से सिद्ध किया।

क्या काम करता है: उन्होंने सफलतापूर्वक ऐसे प्रोग्राम निकाले जो फ़ाइल इनपुट/आउटपुट (फ़ाइलें पढ़ना और लिखना) को संभालते हैं और "रिफाइनमेंट टाइप्स" (अतिरिक्त नियमों वाले प्रकार, जैसे "यह संख्या सकारात्मक होनी चाहिए") का उपयोग करते हैं। उन्होंने दिखाया कि इन जटिल विशेषताओं के साथ भी, एक्सट्रैक्शन सुरक्षित रहता है।
क्या अभी भी प्रगति पर है: शोध पत्र स्वीकार करता है कि उनका वर्तमान सिस्टम रिकर्सिव (recursive) फ़ंक्शंस (वे फ़ंक्शंस जो खुद को कॉल करते हैं) या पूर्ण "डिपेंडेंट टाइप्स" (जहाँ प्रकार मानों पर निर्भर करते हैं) को सबसे स्वाभाविक तरीके से नहीं संभालता है। उन्हें रिकर्सन के लिए इटरेटर्स (लूप्स) का उपयोग करके एक वर्कअराउंड का उपयोग करना पड़ा। वे यह भी नोट करते हैं कि उनके मेटाप्रोग्राम को कभी-कभी यह अनुमान लगाना पड़ता है कि कुछ सुरक्षा जाँच कहाँ रखनी है, जो थोड़ा कठिन हो सकता है।
निष्कर्ष: उन्होंने प्रोग्रामिंग के ब्रह्मांड की हर समस्या को हल नहीं किया है, लेकिन उन्होंने पूर्ण प्रमाणों की दुनिया और वास्तविक कोड की अव्यवस्थित दुनिया के बीच एक नया, बहुत अधिक सुरक्षित पुल बनाया है। उन्होंने सिद्ध किया है कि "रेसिपी लिखने" के चरण और "खाना पकाने" के चरण में काम को विभाजित करके, आप पूर्ण विश्वास के बिना भी मजबूत सुरक्षा गारंटी प्राप्त कर सकते हैं।

संक्षेप में, SEIO★ एक नया उपकरण है जो प्रोग्रामरों को अपने पूर्ण, वेरिफाइड विचारों को वास्तविक दुनिया के सॉफ़्टवेयर में बदलने की अनुमति देता है, जिससे गणितीय रूप से गारंटीकृत सुरक्षा जाल सुनिश्चित होता है, यह सुनिश्चित करते हुए कि भले ही अनुवाद प्रक्रिया अपूर्ण हो, अंतिम परिणाम बाहरी दुनिया की अराजकता से सुरक्षित है।

तकनीकी सारांश: कोटेड नो मोर: IO के साथ F★प्रोग्रामों को सुरक्षित रूप से एक्सट्रैक्ट करना

1. समस्या विवरण (Problem Statement)

F★ एक प्रूफ़-ओरिएंटेड भाषा है जिसका व्यापक रूप से प्रभावों (जैसे, I/O) को दर्शाने के लिए मोनैड्स का उपयोग करके शैलोली एम्बेडेड (shallowly embedded) प्रोग्राम लिखने और सत्यापित करने के लिए उपयोग किया जाता है। एक बार सत्यापित होने के बाद, इन प्रोग्रामों को निष्पादन के लिए OCaml या C जैसी मुख्यधारा की भाषाओं में एक्सट्रैक्ट किया जाता है। हालाँकि, यह एक्सट्रैक्शन प्रक्रिया वर्तमान में अनवेरिफाइड (unverified) है और विश्वसनीय कंप्यूटिंग बेस (TCB) का हिस्सा है।

मुख्य चुनौती "कोटेशन" (quotation) चरण में निहित है जो शैलोली एम्बेडेड प्रोग्रामों को एक्सट्रैक्ट करने के लिए आवश्यक है। कोटेशन में एक शैलोली एम्बेडेड प्रोग्राम (जहाँ प्रभाव मोनैडिक प्रकारों द्वारा दर्शाए जाते हैं) को एक डीपली एम्बेडेड सिंटैक्स ट्री (लक्ष्य भाषा का एक ठोस प्रतिनिधित्व) में अनुवादित करना शामिल है। इस कोटेशन मेटाप्रोग्राम को सत्यापित करना एक बड़ी खुली चुनौती है क्योंकि इसके लिए स्रोत भाषा के लिए एक मैकेनाइज्ड मेटा-थ्योरी की आवश्यकता होती है, और यहाँ तक कि Rocq जैसी परिपक्व प्रणालियों के लिए भी कोटेशन को सत्यापित करना अनसुलझा बना हुआ है।

अनुक्रमण (extraction) को प्रमाणित करने वाले पिछले दृष्टिकोण भारी रूप से ट्रांसलेशन वैलिडेशन (translation validation) पर निर्भर करते हैं, जहाँ एक मेटाप्रोग्राम दोनों मूल कोड और शुद्धता का एक प्रमाण उत्पन्न करता है, जिसे फिर टाइप-चेक किया जाता है। जबकि यह मेटाप्रोग्राम को सत्यापित करने के बजाय TCB को कम करता है, यह अभी भी इस बात पर निर्भर करता है कि मेटाप्रोग्राम वैध प्रमाण उत्पन्न करे, जो विफल हो सकते हैं या गलत हो सकते हैं। इसके अलावा, मौजूदा कार्य मुख्य रूप से शुद्धता (functional correctness) पर ध्यान केंद्रित करते हैं (व्यवहार को बनाए रखना) न कि सुरक्षा (security) पर। जब एक्सट्रैक्ट किए गए कोड को अनवेरिफाइड एडवर्सरियल (adversarial) कोड के साथ जोड़ा जाता है, तो मूल सत्यापित प्रोग्राम के औपचारिक गारंटी से समझौता किया जा सकता है, जिससे अनसोनडनेस (unsoundness) या सुरक्षा उल्लंघन हो सकता है।

2. कार्यप्रणाली (Methodology)

लेखक SEIO★ पेश करते हैं, जो I/O और रिफाइनमेंट प्रकारों वाले F★ प्रोग्रामों को एक डीपली एम्बेडेड सिंपली टाइप्ड $\lambda$ -कैलकुलस ( $\lambda_{io}$ ) में एक्सट्रैक्ट करने के लिए एक फ्रेमवर्क है। कार्यप्रणाली ट्रांसलेशन वैलिडेशन पर निर्भरता को कम करने के लिए निष्कर्षण प्रक्रिया को दो अलग-अलग चरणों में विभाजित करती है:

चरण 1: रिलेशनल कोटेशन (ट्रांसलेशन वैलिडेशन)
सीधे लक्ष्य कोड उत्पन्न करने के बजाय, फ्रेमवर्क एक मेटाप्रोग्राम का उपयोग मूल शैलोली एम्बेडेड प्रोग्राम के लिए एक टाइपिंग डेरिवेशन (typing derivation) उत्पन्न करने के लिए करता है।

रिलेशनल टाइपिंग रिलेशन: लेखक एक टाइपिंग संबंध परिभाषित करते हैं जो एक्सट्रैक्ट किए जा रहे F★ के उपसमुच्चय (जिसे IO★ कहा जाता है) को चित्रित करता है। यह संबंध "ओपन F★ वैल्यूज" (मूल्यों के लिए मूल्यांकन वातावरण वाले फंक्शन) पर कार्य करता है न कि केवल सिंटैक्टिक एक्सप्रेशन पर, जिससे यह शैलो एम्बेडेड प्रोग्राम में फ्री वेरिएबल्स को संभालना संभव होता है।
मेटाप्रोग्राम: एक सरल मेटाप्रोग्राम स्रोत प्रोग्राम की संरचना का पता लगाता है और एक संगत टाइपिंग डेरिवेशन का निर्माण करता है।
वैलिडेशन: उत्पन्न डेरिवेशन को F★ द्वारा टाइप-चेक किया जाता है। क्योंकि टाइपिंग रिलेशन डिपेंडेंट टाइप्स का उपयोग करता है, इसलिए टाइप-चेकर यह सत्यापित करता है कि डेरिवेशन मूल प्रोग्राम के अनुरूप सिंटैक्टिकली और सेमेंटिकली है। यह चरण ही एकमात्र भाग है जो ट्रांसलेशन वैलिडेशन पर निर्भर करता है।

चरण 2: वेरिफाइड सिंटैक्स जनरेशन
एक बार वैध टाइपिंग डेरिवेशन प्राप्त हो जाने के बाद, एक प्योर, वेरिफाइड F★ फंक्शन रिकर्सिवली उस डेरिवेशन का भ्रमण करता है और लक्ष्य $\lambda_{io}$ सिंटैक्स उत्पन्न करता है।

चूंकि टाइपिंग डेरिवेशन, डिपेंडेंट टाइप्स के माध्यम से, स्रोत प्रोग्राम के साथ स्ट्रक्चरल रूप से जुड़ा हुआ है, इसलिए सिंटैक्स जनरेशन फंक्शन यह गारंटी देता है कि उत्पन्न कोड मूल से सेमेंटिक रूप से संबंधित है।
यह चरण पूरी तरह से F★ के भीतर सत्यापित है, जिससे कोड जनरेशन चरण में ट्रांसलेशन वैलिडेशन की आवश्यकता समाप्त हो जाती है।

लॉजिकल रिलेशंस के माध्यम से सुरक्षा गारंटी
सुरक्षा सिद्ध करने के लिए, लेखक स्रोत (IO★) और लक्ष्य ( $\lambda_{io}$ ) भाषाओं के बीच दो क्रॉस-लैंग्वेज लॉजिकल रिलेशंस को परिभाषित करते हैं:

टारगेट-टू-सोर्स: एक लक्ष्य प्रोग्राम को एक स्रोत प्रोग्राम से जोड़ता है, यह सुनिश्चित करता है कि प्रत्येक लक्ष्य व्यवहार का एक संगत स्रोत व्यवहार है।
सोर्स-टू-टारगेट: एक स्रोत प्रोग्राम को एक लक्ष्य प्रोग्राम से जोड़ता है, यह सुनिश्चित करता है कि प्रत्येक स्रोत व्यवहार का एक संगत लक्ष्य व्यवहार है।

ये संबंध ट्रेस-प्रोड्यूसिंग सेमantics (trace-producing semantics) पर परिभाषित हैं, जहाँ I/O ऑपरेशन्स इवेंट्स (ट्रेस) उत्पन्न करते हैं। लेखक सिद्ध करते हैं कि SEIO★ Robust Relational Hyperproperty Preservation (RrHP) को संतुष्ट करता है, जो Abate et al. [1] द्वारा परिभाषित सबसे मजबूत सुरक्षित कंपाइलेशन मानदंड है। RrHP, फुल एब्स्ट्रैक्शन (अवलोकन योग्य तुल्यता का संरक्षण) और मनमाने एडवर्सरियल कॉन्टेक्स्ट के विरुद्ध ट्रेस प्रॉपर्टीज और हाइपरप्रॉपर्टीज (जैसे, नॉनइंटरफेरेंस) के संरक्षण को सुनिश्चित करता है।

रिफाइनमेंट टाइप्स को हैंडल करना
फ्रेमवर्क को रिफाइनमेंट टाइप्स (टाइप्स पर तार्किक बाधाएं) का समर्थन करने के लिए विस्तारित किया गया है। चूंकि F★ रिफाइनमेंट प्रूफ को बिना स्पष्ट प्रूफ टर्म्स के SMT सॉल्वर का उपयोग करके डिस्चार्ज करता है, इसलिए कोटेशन के दौरान रिलेशनल कोटेशन मेटाप्रोग्राम को कमजोर प्रीकंडिशन्स (weakest preconditions) को शुरू से पुनर्गणना करनी पड़ती है और उन्हें फिर से सिद्ध करना पड़ता है ताकि टाइपिंग डेरिवेशन वैध बना रहे।

3. प्रमुख योगदान (Key Contributions)

रिलेशनल कोटेशन: एक नवीन ट्रांसलेशन वैलिडेशन तकनीक जो डिपेंडेंट टाइप्स का उपयोग करके शैलोली एम्बेडेड प्रोग्रामों के लिए एक टाइपिंग रिलेशन को परिभाषित करती है। यह एक मेटाप्रोग्राम को टाइपिंग डेरिवेशन उत्पन्न करने की अनुमति देता जिसे यह सुनिश्चित करने के लिए टाइप-चेक किया जाता है कि वह स्रोत प्रोग्राम के अनुरूप है, जिससे स्वयं मेटाप्रोग्राम को सत्यापित करने की आवश्यकता बच जाती है।
SEIO★ फ्रेमवर्क: I/O और रिफाइनमेंट टाइप्स वाले F★ प्रोग्रामों को एक डीपली एम्बेडेड $\lambda$ -कैलकुलस में एक्सट्रैक्ट करने के लिए एक पूर्ण निष्कर्षण फ्रेमवर्क।
फॉर्मल सिक्योर कंपाइलेशन: F★ में एक मशीन-चेक्ड प्रूफ कि SEIO★ RrHP को संतुष्ट करता है। यह प्रमाण-उन्मुख भाषाओं के लिए ऐसा मजबूत सुरक्षा आश्वासन प्रदान करने वाला पहला निष्कर्षण फ्रेमवर्क है।
क्रॉस-लैंग्वेज लॉजिकल रिलेशंस: दो एसिमेट्रिक लॉजिकल रिलेशंस की परिभाषा और प्रमाण जो ट्रेस-प्रोड्यूसिंग सेमantics वाले शैलोली एम्बेडेड भाषा और मानक ऑपरेशनल सेमantics वाली डीपली एम्बेडेड भाषा के बीच के अंतर को पाटते हैं।
रिफाइनमेंट टाइप सपोर्ट: कोटेशन के दौरान प्रीकंडिशन्स को पुनर्गणना और पुन: सत्यापित करके रिफाइनमेंट टाइप्स को संभालने के लिए फ्रेमवर्क का विस्तार।

4. परिणाम (Results)

लेखकों ने 900 से अधिक टॉप-लेवल डेफिनिशन के साथ F★ में SEIO★ को लागू किया।
उन्होंने एक रनिंग एग्जांपल को सफलतापूर्वक एक्सट्रैक्ट किया: एक वैलिडेशन रैपर जो अनवेरिफाइड AI एजेंट्स के लिए है, जो एक फाइल पढ़ता है, एक एजेंट को कॉल करता है, और परिणाम को सत्यापित करता है।
फ्रेमवर्क का परीक्षण सीधे लक्ष्य $\lambda_{io}$ भाषा में लिखे गए विभिन्न एजेंट्स (सही और दुर्भावनापूर्ण दोनों) के साथ किया गया।
मशीन-चेक्ड प्रूफ पुष्टि करता है कि निष्कर्षण सुरक्षा गुणों को बनाए रखता है, भले ही इसे मनमाने अनवेरिफाइड कोड के साथ जोड़ा गया हो, जो RrHP को संतुष्ट करता है।
आर्टिफैक्ट में Peregrine फ्रेमवर्क और Malfunction का उपयोग करके एक्सट्रैक्ट किए गए $\lambda_{io}$ कोड को OCaml में कंपाइल करने के लिए एक पाइपलाइन शामिल है, जिससे व्यावहारिक निष्पादन संभव होता है।

5. महत्व और दावे (Significance and Claims)

यह पेपर दो प्रमुख तरीकों से अत्याधुनिक स्थिति (state of the art) को आगे बढ़ाने का दावा करता है:

ट्रांसलेशन वैलिडेशन को कम करना: ट्रांसलेशन वैलिडेशन को टाइपिंग डेरिवेशन (रिलेशनल कोटेशन) के निर्माण तक सीमित करके और उसके बाद के सिंटैक्स जनरेशन चरण को सत्यापित करके, फ्रेमवर्क पिछले सर्टिफाइंग एक्सट्रैक्शन कार्यों की तुलना में अनवेरिफाइड मेटाप्रोग्रामों पर निर्भरता को कम करता है।
शुद्धता पर सुरक्षा: पिछले कार्यों के विपरीत जो कार्यात्मक शुद्धता (functional correctness) पर केंद्रित थे, SEIO★ औपचारिक सुरक्षित कंपाइलेशन गारंटी प्रदान करता है। यह सुनिश्चित करता है कि सत्यापित F★ प्रोग्राम अपने सुरक्षा गुणों (जैसे, नॉनइंटरफेरेंस और ट्रेस प्रॉपर्टीज) को बनाए रखते हैं, भले ही उन्हें मनमाने, अनवेरिफाइड या एडवर्सरियल कोड के साथ जोड़ा गया हो।

लेखक नोट करते हैं कि यह कार्य वर्तमान अत्याधुनिक स्थिति से आगे जाता है, जिसने अभी तक प्रमाण-उन्मुख भाषाओं से निष्कर्षण के लिए ऐसी मजबूत सुरक्षित कंपाइलेशन गारंटी प्रदान नहीं की है। वे सीमाओं को स्वीकार करते हैं, जैसे कि सामान्य रिकर्सिव फंक्शन्स और पूर्ण डिपेंडेंट टाइप्स के लिए वर्तमान समर्थन की कमी, जिन्हें भविष्य के कार्य के रूप में छोड़ दिया गया है। पेपर इस बात पर जोर देता है कि हालांकि रिलेशनल कोटेशन मेटाप्रोग्राम अनवेरिफाइड है, इसकी सरलता और उसके बाद के चरणों का कठोर सत्यापन समग्र दृष्टिकोण को मजबूत बनाता है।