Vi minskar klyftan mellan konkreta implementeringar av kryptografiska protokoll och deras verifierade modeller. Vi utvecklar och verifierar ett litet funktionellt genomförande av Transport Layer Security Protocol (TLS 1.0). Vi använder samma körbara kod för driftskompatibilitetstester mot vanliga implementationer för automatiserad symbolisk kryptografisk verifiering och automatiserad beräkningskryptografisk verifiering. Vi förlitar oss på en kombination av nya verktyg och utvecklar också ett nytt verktyg för att extrahera beräkningsmodeller från körbar kod. Vi får starka säkerhetsgarantier för TLS som används i typiska driftsättningar.  Det har gjorts stora framsteg på senare tid när det gäller formella metoder och verktyg för kryptografi, vilket möjliggör automatisk verifiering av komplexa säkerhetsprotokoll. I praktiken är det dock svårt att tillämpa dessa metoder och verktyg. Ofta sker verifieringen oberoende av utvecklingsprocessen, snarare än under konstruktion, prototypering och testning. Allteftersom ett protokoll eller dess genomförande utvecklas är det också svårt att överföra säkerhetsgarantier från tidigare formella kontroller. Verifieringen av ett system som använder ett visst protokoll innebär dessutom mer än en kryptografisk verifiering av en abstrakt modell; det kan också förlita sig på mer standardanalyser av kod (t.ex. för att säkerställa minnessäkerhet) och systemkonfiguration (t.ex. för att upprätthålla policyn). Av dessa skäl är vi intresserade av att integrera moderna kryptografiska protokollkontrollanter i arsenalen av testnings- och verifieringsverktyg för programvara. Genomföranden mot abstrakta modeller. Protokollspecifikationerna innehåller många detaljer, varav de flesta (men inte alla) inte har någon betydelse för säkerheten. I processen att destillera en formell kryptografisk modell, de flesta av dessa detaljer kastas. När förenklas en protokollmodell? I motsats till de formella garantierna inom modellen bygger modellens relevans på formalistens erfarenhet. Problemet förvärras när man överväger protokollgenomföranden. Därför föreslår vi att man så långt det är möjligt kontrollerar detaljerade protokollgenomföranden och införanden i stället för handskrivna abstrakta modeller. Genom att använda automatiserade verktyg baserade på ljudisolerade tekniker kan detaljerna antingen raderas säkert eller hanteras av brute-force analys. Bhargavan m.fl. [2006] kontrollera protokoll implementeringar skrivna i F#, en dialekt ML för.NET runtime, genom sammanställning till symboliska modeller i ProVerif [Blanchet 2001]. Deras tillvägagångssätt verifierar så mycket protokollkod som möjligt samtidigt som de tillhandahåller handskrivna modeller för resten, såsom de centrala biblioteken som tillhandahåller kryptografiska primitiva, med hjälp av bitsträngar för konkret utförande och symboliska termer för verifiering. I detta arbete förlitar vi oss på deras verktyg för symbolisk verifiering och även experimentera med direkta beräknings kryptografiska verifieringar av protokoll implementeringar genom sammanställning till CryptoVerif, ett nytt verktyg för beräknings kryptografi [Blanchet 2008]. Vår strategi. Figur 1 illustrerar vår allmänna strategi för att utveckla, testa och verifiera ett referensgenomförande av ett protokoll, plus en typisk tillämpning. I motsats till användningen av specialiserade modelleringsspråk för kryptografiska protokoll, gör vår användning av en standardutvecklingsplattform det möjligt att tidigt testa specifikationen, bekräfta funktionell korrekthet, och experimentera med potentiella attacker, bland annat fördelar. Verifiering består av att välja en del av genomförandet och skriva ytterligare verifieringssel kod som specificerar angriparmodellen, kryptografiska antaganden, och mål säkerhetsegenskaper, och sedan sammanställa sin kombination till några automatiserade bevis. Eftersom verifieringsverktygskedjan är automatiserad kan man enkelt kontrollera kodbasen när den utvecklas, ungefär som regressionstest. Enligt vår erfarenhet kompletterar symboliska och beräkningsmässiga verifieringar varandra. Beräkningsverifiering är mer exakt men också svårare att uppnå; vi får resultat endast för den kryptografiska kärnan i protokollets genomförande. Symbolisk verifiering gäller vanligtvis för hela protokollet, ibland även inklusive programmet, men inte upptäcka låg nivå kryptografiska fel. Sammantaget tror vi att omkostnaderna för formell verifiering blir överkomliga i jämförelse med design, utveckling och testning. Nästa generation verktyg skulle kunna göra det möjligt att integrera dem i utvecklingsprocessen. Genomförande och verifiering av TLS. Som en utvidgad fallstudie behandlar denna artikel genomförandet av TLS 1.0, ett av de mest utbredda kommunikationsprotokollen. På grund av dess popularitet, många system inbäddade en implementering av TLS och förlitar sig på sin säkerhet för kommunikation. Förutom att vara av praktisk betydelse, är TLS ett välförståeligt protokoll med en noggrant skriven, fristående specifikation, en serie på varandra följande versioner, och en stor mängd relaterade verifieringsarbete, vilket ger en detaljerad historik över säkerhetssårbarheter och förbättringar. TLS är inte ett akademiskt protokoll, optimerat (eller utformat) för verifieringsändamål. Detta komplicerar ibland säkerhetsanalysen, men utgör också ett bra riktmärke för bedömning av kontrollmetoder. (1) Vi programmerar ett litet, funktionellt genomförande av TLS i F#. Med hjälp av enkel klient- och serverkod bekräftar vi att den samarbetar med vanliga implementationer. (2) Genom att förlita oss på en kombination av verktyg för modellextraktion och verifiering får vi en rad positiva säkerhetsresultat, som omfattar både symboliska och beräkningsmässiga kryptografiska aspekter av protokollet. Vi ger alltså säkerhetsgarantier för kod eftersom den används i typiska distributioner av TLS. (3) För att stödja beräkningsverifiering utvecklar vi ett nytt verktyg för att extrahera kryptografiska modeller från F#-koden. Såvitt vi vet möjliggör detta den första automatiska verifieringen av körbar kod enligt standardiserade kryptografiska antaganden. (4) Vi granskar kända svagheter för tidigare varianter av TLS och bekräftar att de exponeras när vi försöker verifiera motsvarande försvagade varianter av vår kod. Innehåll. I avsnitt 2 erinras om de viktigaste säkerhetsdetaljerna i TLS. I avsnitt 3 diskuteras genomförandet av referensprotokollet i ML. I avsnitt 4 beskrivs vårt genomförande av TLS, dess huvudmoduler, TLS och rapporter om driftskompatibilitet. Avsnitt 5 presenterar våra resultat med hjälp av symboliska modeller; det diskuterar också formella säkerhetsfrågor
Sådana översättningar har använts för att symboliskt och beräkningsmässigt analysera TLS implementationer REF.
Verified Cryptographic Implementations for TLS
{'venue': 'TSEC', 'journal': None, 'mag_field_of_study': ['Computer Science']}