Proof-carrying code (PCC, în traducere literală „cod cu demonstrație atașată”) este o tehnică de securitate și verificare formală prin care un sistem-gazdă poate verifica proprietăți ale unui program înainte de executarea acestuia. Codul executabil este livrat împreună cu o demonstrație formală care arată că programul respectă o anumită politică de siguranță. Gazda verifică demonstrația și compară concluziile ei cu propria politică de securitate; dacă verificarea reușește, codul poate fi executat fără verificări suplimentare la rulare pentru proprietățile acoperite de demonstrație. O utilizare tipică este verificarea siguranței memoriei, de exemplu pentru a preveni accesări în afara limitelor unor zone de memorie, inclusiv erori de tip buffer overflow.

Conceptul a fost introdus în lucrări publicate de George C. Necula și Peter Lee în 1996; articolul lui Necula despre PCC a fost publicat apoi la POPL 1997.

Exemplul filtrului de pachete Lucrarea din 1996 despre extensii sigure ale nucleului a folosit filtre de pachete ca exemplu experimental. În acest caz, un filtru de pachete este o subrutină furnizată de aplicație, apelată de nucleu pentru fiecare pachet de rețea primit în cod mașină care decide dacă aplicația este interesată să proceseze un anumit pachet de rețea. Deoarece filtrul rulează în mod kernel, un filtru malițios sau defect ar putea afecta integritatea sistemului dacă ar avea posibilitatea să scrie arbitrar în structurile de date ale nucleului.

Soluțiile comparate de Necula și Lee includeau filtre bazate pe Berkeley Packet Filter, izolarea defectelor prin software și implementări în limbaje considerate sigure, precum Modula-3. Pentru cod executat foarte frecvent, cum este un filtru de pachete, aceste metode pot introduce costuri de performanță; în varianta PCC, costul principal este verificarea demonstrației la încărcarea codului, nu la fiecare execuție a filtrului.

În abordarea PCC, nucleul publică o politică de siguranță pe care orice filtru trebuie să o respecte. Pentru un filtru de pachete, politica poate cere ca filtrul să nu acceseze memorie în afara pachetului și a unei zone auxiliare de memorie alocate pentru acesta. Un demonstrator de teoreme este folosit pentru a arăta că instrucțiunile în cod mașină respectă politica. Pașii demonstrației sunt atașați codului, iar încărcătorul de programe al nucleului verifică demonstrația înainte de executare. Dacă un atacator modifică fie codul, fie demonstrația, verificarea eșuează sau demonstrația rămasă validă continuă să garanteze respectarea politicii de siguranță.

Vezi și

Note

Categorie:Metode formale Categorie:Securitate informatică