Proof-carrying code (PCC) – бағдарламаның қауіпсіздігін растайтын, формальды дәлелдермен жұмыс істейтін құрал. Жады қауіпсіздігін қамтамасыз етеді. 🛡️💻
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Proof carrying code (PCC) — бағдарламалық қамтамасыз ету механизмі, ол хост-жүйеге қосымшаның орындалатын кодымен бірге келген формальді дәлелдеме арқылы қосымша туралы қасиеттерін тексеруге мүмкіндік береді. Хост-жүйе дәлелдеменің дұрыстығын жылдам тексеріп, дәлелдеменің қорытындыларын өзінің қауіпсіздік саясатымен салыстыра отырып, қосымшаны орындау қауіпсіз екенін анықтай алады. Бұл, әсіресе, жад қауіпсіздігін қамтамасыз етуде (мысалы, буфер асығу сияқты мәселелерді болдырмау) өте пайдалы. Proof carrying code алғаш рет 1996 жылы Джордж Некула және Питер Ли есімді ғалымдар сипаттаған.
Proof carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the proof, and it can compare the conclusions of the proof to its own security policy to determine whether the application is safe to execute. This can be particularly useful in ensuring memory safety (i. e. preventing issues like buffer overflows). Proof carrying code was originally described in 1996 by George Necula and Peter Lee.
Пакет сүзгісінің мысалы
1996 жылы дәлелді кодты тасымалдау туралы алғашқы жарияланымда пакет сүзгілері мысал ретінде келтірілді: пайдаланушы режиміндегі бағдарлама ядроға машиналық кодта жазылған функцияны жібереді, ол белгілі бір желілік пакетті өңдеуге қызығушылық танытатынын анықтайды. Пакет сүзгісі ядролық режимде жұмыс істейтіндіктен, егер ол ядролық дерек құрылымдарына жазатын қауіпті кодты қамтыса, жүйенің қауіпсіздігіне нұқсан келтіруі мүмкін. Бұл мәселеге қатысты дәстүрлі тәсілдерге пакет сүзгілеу үшін арнайы домендік тілді интерпретациялау, әр жадқа қол жеткен кезде тексерулер енгізу (бағдарламалық қателерді оқшаулау) және сүзгіні жоғары деңгейдегі тілде жазу кіреді, ол орындалу алдында ядрода компиляцияланады. Бұл тәсілдер пакет сүзгісі сияқты жиі орындалатын код үшін өнімділік кемшіліктеріне ие, ядролық компиляция тәсілінен басқа, ол кодты тек жүктелген кезде ғана компиляциялайды, әр орындалу сайын емес. Дәлелді кодты тасымалдау арқылы ядро кез келген пакет сүзгісі сақтауы тиіс қасиеттерді көрсететін қауіпсіздік саясатын жариялайды: мысалы, пакет сүзгісі пакет пен оның қосымша жады аймағынан тыс жадқа қол жеткізе алмайды. Теореманы дәлелдейтін құрал машиналық кодтың осы саясатты орындауын көрсету үшін қолданылады. Осы дәлелдеу қадамдары жазылып, ядролық бағдарлама жүктеушіге берілетін машиналық кодқа қоса беріледі. Бағдарлама жүктеуші дәлелді жылдам тексеруге және одан кейін қосымша тексерулерсіз машиналық кодты орындауға мүмкіндік береді. Егер қауіпті тұлға машиналық кодты немесе дәлелдемені өзгертетін болса, нәтижесіндегі дәлелді код жарамсыз болады немесе зиянсыз болып қалады (әлі де қауіпсіздік саясатын сақтайды).
The original publication on proof carrying code in 1996 used packet filters as an example: a user mode application hands a function written in machine code to the kernel that determines whether or not an application is interested in processing a particular network packet. Because the packet filter runs in kernel mode, it could compromise the integrity of the system if it contains malicious code that writes to kernel data structures. Traditional approaches to this problem include interpreting a domain specific language for packet filtering, inserting checks on each memory access (software fault isolation), and writing the filter in a high level language which is compiled by the kernel before it is run. These approaches have performance disadvantages for code as frequently run as a packet filter, except for the in kernel compilation approach, which only compiles the code when it is loaded, not every time it is executed. With proof carrying code, the kernel publishes a security policy specifying properties that any packet filter must obey: for example, the packet filter will not access memory outside of the packet and its scratch memory area. A theorem prover is used to show that the machine code satisfies this policy. The steps of this proof are recorded and attached to the machine code which is given to the kernel program loader. The program loader can then rapidly validate the proof, allowing it to thereafter run the machine code without any additional checks. If a malicious party modifies either the machine code or the proof, the resulting proof carrying code is either invalid or harmless (still satisfies the security policy).