I scenarier som webbprogrammering, där kod kopplas samman från flera källor, ger objektkapacitetsmönster ett viktigt skydd, vilket gör det möjligt för programmerare att skydda det privata tillståndet hos sina objekt från korruption genom okänd och opålitlig kod. Fördelarna med OCP:er när det gäller programverifiering har dock aldrig blivit ordentligt formaliserade. I detta dokument, som bygger på den nyligen utvecklade Iris-ramen för samtidig separationslogik, utvecklar vi OCPL, den första programlogiken för kompositionsbestämning och verifiering av OCP:er på ett språk med stängningar, muterbara tillstånd och samstämmighet. Den viktigaste idén med OCPL är att redogöra för gränssnittet mellan verifierad och opålitlig kod genom att anta en välkänd idé från litteraturen om verifiering av säkerhetsprotokoll, nämligen robust säkerhet. Program som exporterar endast rätt inpackade värden till sin miljö kan bevisas robust säkert, vilket innebär att deras opålitliga miljö inte kan bryta mot deras interna invarianter. Vi använder OCPL för att ge de första allmänna, kompositions- och maskinkontrollerade specifikationerna för flera vanliga OCPs — inklusive dynamisk tätning, membran, och vaktmästare mönster — som vi sedan använder för att verifiera robust säkerhet för representativ kundkod. Alla våra resultat är helt mekaniserade i Coq bevis assistent.
Mycket nyligen, Swasey et al. REF föreslår den första programlogiken som kan kompositionellt specificera och verifiera objektets kapacitetsmönster i JavaScript-liknande språk.
Robust and compositional verification of object capability patterns
{'venue': 'PACMPL', 'journal': None, 'mag_field_of_study': ['Computer Science']}