Distribuerade applikationer kan struktureras som parter som utbyter meddelanden enligt vissa förutbestämda kommunikationsmönster. Dessa sessioner (eller kontrakt, eller protokoll) förenklar distribuerad programmering: när man kodar en roll för en viss session, måste varje part bara följa det avsedda meddelandeflödet, under antagandet att de andra parterna också uppfyller kraven. I en kontradiktorisk situation kan man inte lita på att avlägsna parter spelar sin roll. Därför måste defensiva implementationer också övervaka varandra, för att upptäcka eventuella avvikelser från de tilldelade rollerna för en session. Denna uppgift innebär låg nivå kodning under session abstraktioner, vilket ger upp de flesta av sina fördelar. Vi utforskar språkbaserat stöd för sessioner. Vi utökar ML-språket med sessionstyper som uttrycker flöden av meddelanden mellan roller, så att välskrivna program alltid spelar sina roller. Vi sammanställer sessionstypdeklarationer till kryptografiska kommunikationsprotokoll som kan skydda program från alla lågnivåförsök från koalitioner av fjärrkollegor att avvika från sina roller. Vårt huvudsakliga resultat är att när man resonerar om program som använder vår sessionsimplementation, kan man säkert anta att alla sessionskamrater följer sina roller utan att lita på deras fjärrimplementationer. Programmeringsnätverk, oberoende system är komplexa, eftersom programmeraren har liten kontroll över körtidens miljö. För att förenkla sin uppgift erbjuder programmeringsspråk och systembibliotek abstraktioner för gemensamma kommunikationsmönster (t.ex. privata kanaler eller RPC), med automatiserat stöd för att hjälpa programmeraren att använda dessa abstractioner på ett tillförlitligt sätt och för att befria honom från deras lågnivåuppgifter (t.ex. meddelandeformat och routing). Som ett exempel, webbtjänster främja deklarativa typer och policyer för meddelanden, med verktyg som automatiskt kan hämta dessa deklarationer och ställa in proxies med en enkel typad programmeringsgränssnitt. Ur ett säkerhetsperspektiv, när delar av systemet och vissa av de avlägsna parterna inte är betrodda, kan kommunikationsabstractioner vara särskilt effektiva: beroende på kryptografiska protokoll, kan implementationer av dessa abstractioner ibland helt skydda programmerare från attacker på låg nivå (t.ex. meddelandeavlyssning och omskrivning) [1, 2]. Detta är dock sällan fallet i praktiken, eftersom säkerheten tvingar programmeraren att förstå lågnivåprotokollfrågor. Utöver enkla abstraktioner för kommunikation, kan distribuerade applikationer ofta struktureras som parter som utbyter meddelanden enligt vissa fasta, i förväg arrangerade mönster. Dessa sessioner (även namngivna kontrakt, arbetsflöden, eller protokoll) förenklar distribuerad programmering genom att ange beteendet hos varje nätverksenhet, eller roll. Genom att komma överens om en gemensam mötesspecifikation kan parterna lösa det mesta av komplexiteten i förväg. Sedan, när kodning en roll för en viss session, måste varje part bara följa meddelandet flöde för denna roll, under antagandet att de andra parterna också är förenliga. På run-time, sessioner kan äntligen bli omedelbar genom att kartlägga roller till faktiska rektorer och deras värdar. Språkbaserat stöd för sessioner är föremål för aktiv forskning [7, 8, 9, 13, 16, 30, 32]. I synnerhet flera av de senaste typerna av system säkerställer statisk överensstämmelse med sessionsspecifikationerna. I deras inställning, typ säkerhet innebär att användarkoden som omedelbart en session roll alltid beter sig som föreskrivs i sessionen. Således, förutsatt att varje distribuerat program som kan delta i en session är väl-typad, alla körningar av sessionen följer dess specifikation. I en kontradiktorisk situation kan man inte lita på att avlägsna parter spelar sin roll. Därför måste defensiva implementationer också övervaka varandra, för att förhindra all förvirring mellan parallella sessioner, för att säkerställa autentisering, korrelation och orsakssamband mellan meddelanden och, mer allmänt, för att upptäcka eventuella avvikelser från de tilldelade rollerna för en session. Överlämnad till programmeraren innebär denna uppgift en känslig kodning på låg nivå under sessionens abstraktioner, vilket besegrar deras syfte. Istället föreslår vi att systematiskt sammanställa sessionsspecifikationer till kryptografiska protokoll. I detta dokument undersöker vi språkbaserat stöd för sessioner och deras genomförande, enligt följande: 1. Vi utformar ett litet inbäddat språk av typer för att specificera meddelanden, roller och sessioner, och vi identifierar en säker implementering villkor för dessa sessioner. 2. Utgångspunkten är följande: Vi utökar F# [28] (en dialekt av ML [23, 24]) med distribuerad kommunikation och sessioner, så att typ säkerhet ger funktionella garantier: varje skickat meddelande förväntas av dess mottagare, med matchande nyttolast typer. 3. Vad är det som händer? Vi sammanställer sessionstyper till kryptografiska kommunikationsprotokoll, kodade i F#, som kan skydda våra program från alla försök av koalitioner av fjärrkollegor att avvika från sina roller. På så sätt får vi ett säkert, funktionellt, distribuerat genomförande av sessioner. 4. Vad är det som händer? Vårt huvudteorem säger att de säkerhetsgarantier som underförståtts av sessionstyper inte beror på genomförandet av några avlägsna kamrater: ur synvinkelt av våra distribuerade program, kan alla åtgärder som kan inträffa också ske i en abstrakt miljö, med hjälp av ett centraliserat genomförande som upprätthåller alla sessionstyper. Till vår kännedom ger detta dokument det första säkra genomförandet av sessionstyper, både formellt och konkret. Det relaterar semantik av tre språk: på nivå av typer, enkla processer för att specificera kommunikationsmönster och nyttolaster; som ett källspråk, en delmängd av F# med distribuerad kommunikation och maskinskrivna sessioner; som ett genomförandespråk, en delmängd av F# med distribuerad kommunikation och kryptografi. Vår kompilator extraherar sessionsdefinitioner, verifierar att de uppfyller den säkra implementeringen villkor, genererar motsvarande kryptografiska protokoll, och avger sin kod som F# moduler. Å andra sidan lämnar den koden som använder sessioner oförändrad, behandla sessionskonstruktioner av det utvidgade språket som vanliga högre ordning funktion kallar till deras implementeringar. Därför ringer användarkoden vår genererade kod för att ange en session och sedan, för varje mottagna meddelande, genererade kod samtal tillbaka användarkod och återupptar protokollet när användarkoden returnerar nästa meddelande som ska skickas. Att dra nytta av denna anropskonvention, med en separat typad användarkod fortsättning för varje tillstånd av varje roll i sessionen, kan vi således helt lita på att vanliga skrivaà la ML att genomdriva session skriva i användarkod. (I det följande, eftersom vi fokuserar på sessionssäkerhet, behandlar vi denna viktiga men välförstådda aspekt av sessionstyper informellt.) De sammanställda protokollen bygger på en kombination av standardtekniker för autentisering och anti-replay skydd. Kompilatorn introducerar inget ytterligare meddelande: varje abstrakt sessionsmeddelande avbildas till ett kryptografiskt meddelande med samma avsändare och mottagare. Rektorerna är autentiserade med X.509 certifikat. Alla meddelanden innehåller en unik sessionsidentifierare (finns som gemensam kryptografisk hash av sin sessionstyp, dess tilldelning av uppdragsgivare till roller och en ny sessionsnunce) och en serie av signaturer: en signatur från meddelandeavsändaren, plus en vidarebefordrad signatur från varje deltagare som deltar i sessionen sedan mottagarens senaste meddelande (eller början av sessionen). När som helst i en session, varje protokoll roll vet exakt vilka meddelanden att förvänta sig och vad de bör innehålla, så att vi kan använda kompakta trådformat och kompilera enkla, specialiserade meddelandehanterare. Varje meddelande som avviker från det förväntade formatet kan tyst tappas, eller på ett tillförlitligt sätt detekteras som avvikande. Säkerheten för automatiskt genererade kryptografiska protokoll implementeringar är avgörande beroende av formell verifiering. I detta syfte bygger vår språkdesign och prototypimplementering på Bhargavan et al. [4], som minskar klyftan mellan den konkreta körbara koden och dess verifierade modell. Vår genererade kod beror på bibliotek för nätverk, kryptografi, och principer, med dubbla implementationer. En konkret implementering använder standard kryptografisk algoritmer och nätverk primitiver; den producerade koden stöder distribuerad körning. En andra, symbolisk implementering definierar kryptografi med algebraiska datatyper, i Dolev-Yao stil; den producerade koden stöder samtidig körning, och är också vår formella modell. Således våra säkerhet teorem gäller direkt för godtycklig användarkod som kallar vår session-genererad kod som kallar vår symboliska bibliotekskod, inom en formell modell av en delmängd av F# (snarare än en ad-hoc abstrakt modell av protokollet löst relaterad till faktiska körbar kod). Relaterat arbete Sessionstyper har utforskats först för processkalkyl [17, 20, 32], för att beskriva interaktion på enstaka kanaler. Beteendetyper [9, 21] stöder mer uttrycksfulla sessioner, som skrivs in som CCS-processer som eventuellt involverar flera kanaler. Ett annat typsystem [6] kombinerar också sessionstyp och korrespondenspåståenden [19]. Nya verk överväga tillämpningar av sessionstyper till konkreta inställningar såsom CORBA [29], ett multi-trådat funktionellt språk [30], och ett distribuerat objekt-orienterat språk [13]. Framför allt undersöker Singularity OS [16] användningen av maskinskrivna kontrakt i utformningen och genomförandet av operativsystemet. I alla dessa arbeten används typsystem för att säkerställa sessionsöverensstämmelse inom helt betrodda system, exklusive närvaron av en (aktiv, otypad) angripare. Sessioner för webbtjänster beaktas för WSDL- och WS-SecureConversation Specification languages (se t.ex. [3, 8] ben et al. [7] också presentera ett språk för att beskriva webbinteraktioner från ett globalt perspektiv och beskriva deras endpoint-projektion till lokala rollbeskrivningar. Deras tillvägagångssätt liknar vår behandling av sessionsgrafer och roller i Avsnitt 2, men deras beskrivningar är körbara program, inte typer. Mer allmänt, distribuerade språk som akut och HashCaml [26, 12, 5 ] är också beroende av typer för att ge allmänna funktionella garantier för nätverkade program, särskilt typ säker rangering och dynamisk återbindning till lokala resurser. Cryptographic communications protokoll har studerats grundligt, så vi fokuserar på relaterade arbete på deras användning för att säkerställa implementeringar av programmering-språk abstraktioner. De kan tillhandahålla säkra implementationer för distribuerade språk med privata kommunikationskanaler [1, 2]. De kan också hjälpa till att stödja distribuerat genomförande av sekventiella språk som JIF/Split [33], samtidigt som man bevarar hög nivå, skrivbar integritet och sekretessgarantier. På liknande sätt sammanställer Fairplay [22]-systemet procedurbeskrivningar på hög nivå för att säkra tvåpartsberäkningar. I annat arbete genomdrivs typbaserad sekretess och integritetsgarantier genom en kombination av statisk typkontroll och sammanställning till kryptografisk verksamhet på låg nivå [15]. Protokollsyntes och omvandling har undersökts i andra inställningar: till exempel, Automatic Protocol Generation (APG) verktyg [25] genererar autentisering protokoll sedan verifieras med Athena [27] och, mer nyligen, Cortier et al. [11] kontrollera att en generisk omvandling är korrekt för att skydda ett protokoll från aktiva attacker (men inte från utsatta deltagare). Innehåll Avsnitt 2 definierar två vyer av sessioner, som globala kommunikationsdiagram och som lokala rolldefinitioner. Avsnitt 3 ger (rättvis standard) syntax och semantik för våra käll- och målspråk. Avsnitt 4 beskriver de bibliotek som bäddar in våra antaganden om kryptografi och principer, som används i vårt genomförande. Avsnitt 5 presenterar vårt optimerade kryptografiska protokoll, som en förfining av ett grundläggande, intuitivt säkert protokoll. Avsnitt 6 beskriver vår tillämpningskod för sessioner. I avsnitt 7 anges våra viktigaste resultat, som formellt visar att genomförandet är korrekt. Avsnitt 8 avslutas. Bilagan innehåller ytterligare information om vårt genomförande, inklusive listor för utvalda bibliotek. Ett följepapper innehåller också ett detaljerat programmeringsexempel och alla bevis [10].
Arbetet i REF liknar i andemeningen vårt, men skiljer sig i begrepp och detaljer, eftersom det använder en sessionsgraf specifikation för att generera en kryptografisk funktionell implementation som har session integritet.
Secure Implementations for Typed Session Abstractions
{'venue': "20th IEEE Computer Security Foundations Symposium (CSF'07)", 'journal': "20th IEEE Computer Security Foundations Symposium (CSF'07)", 'mag_field_of_study': ['Computer Science']}