Abstrakt. Informationsflöde politik kan uttrycka starka säkerhetskrav för program som drivs av distribuerade parter med olika nivåer av förtroende. Denna säkerhet är dock svår att bevara när program kompileras till distribuerade system med (potentiellt) komprometterade maskiner. Många program inbegriper till exempel beräkningar som är alltför känsliga för att man skall kunna lita på någon av dessa maskiner. Många program är inte heller helt säkra (icke-inblandning); eftersom de selektivt stöder och avklassificerar information blir deras relativa säkerhet svårare att bevara. Vi utvecklar en säker kompilator för distribuerade informationsflöden. För att minimera förtroendeantaganden förlitar vi oss på kryptografiskt skydd, och vi utnyttjar hårdvara och programvarumekanismer som finns tillgängliga på moderna arkitekturer, såsom säkra kängor, betrodda plattformsmoduler och fjärrintyg. Vi presenterar en säkerhetsmodell för dessa mekanismer på ett absolut nödvändigt språk med dynamisk kodbelastning. Vi definierar programomvandlingar för att generera betrodda virtuella värdar och för att köra dem på opålitliga maskiner. Vi får sekretess och integritet teorem under realistiska antaganden, visar att det sammanställda distribuerade systemet är minst lika säker som källprogrammet. När man utformar eller ser över ett systems säkerhet är ett första steg att identifiera dess tillförlitliga datorbas (TCB), dvs. den uppsättning komponenter som man måste lita på för att uppnå en viss säkerhetsnivå. För generella nätverksmaskiner är denna uppsättning stor och komplex; den innehåller hårdvara, ett operativsystem, en körtid miljö och deras bibliotek (kan vara 10 8 LOCs totalt) plus drivrutiner, applikationer, och dynamiskt laddad kod. Detta leder till en bästa insats för säkerhet, i motsats till formell verifiering, som ger starka garantier endast för mindre, enklare system. Minimala TCB:er. Moderna datorarkitekturer ger hårdvarustöd för att minska TCB:er och skydda privilegierade verksamheter. Således de flesta datorer levereras med någon form av säker coprocessor med en dedikerad säker instruktion set-till exempel, de flesta bärbara datorer nu inbäddade en Trusted Platform Module (TPM) (TCG, 2005) och många high-end processorer har en speciell sen lanseringsfunktion (AMD: s Secure Virtual Machine Architecture, 2005, och Intels Trusted Execution Technology, 2009). Dessa instruktioner kan köra en viss kod i isolering, med stark kodbaserad identitet och privilegierade kryptografiska operationer, till exempel för att försegla ihållande tillstånd eller utföra fjärrtillstånd. Sådana hårdvarumekanismer kan kraftigt minska TCB av säkerhetsapplikationer, genom att ta bort behovet av att lita på värdoperativsystemet och andra program, och därmed bidra till att skydda kritiska data och beräkningar från skadlig programvara. TPM används rutinmässigt för säker uppstart, t.ex. BitLocker (Microsoft, 2006) vakter tillgång till huvudnycklarna för diskkryptering, så att diskinnehållet kan läsas först efter autentisering användaren och operativsystemet. Även forskningsrapporter beskriver t.ex. Hur man bygger säkra online betalningssystem (Balfe och Paterson, 2008) och hur man använder sena lanseringar för att köra små bitar av applikationskod i isolering (McCune et al., 2008 (McCune et al.,, 2009 ). Ändå används de säkra instruktionerna anmärkningsvärt sällan i praktiken. Vi anser att komplexiteten i deras låga nivå gränssnitt och bristen på programmeringsverktyg är stora hinder för deras vanliga antagande för att skriva säkerhetsapplikationer. Informationsflödessäkerhet. På en mer abstrakt nivå förlitar sig språkbaserad säkerhet ofta på informationsflödespolitik (Denning, 1976; Myers och Liskov, 2000). Varje variabel tilldelas en nivå i en säkerhetslattice; denna nivå anger den avsedda integriteten och sekretessen för all information som lagras i denna variabel. Således anses ett program helt säkert (icke-inblandning) om en motståndare som endast kan få tillgång till information på låg nivå inte kan få (eller påverka) någon information på högre nivå genom att utföra programmet. Statiska analyser och typsystem har utvecklats för att verifiera att ett program är säkert med avseende på en viss policy. Dessutom är det ibland möjligt att sammanställa sådana program till ett givet system samtidigt som deras säkerhetsegenskaper bevaras. Därför erbjuder Jif och FlowCaml (Pottier och Simonet, 2003) säkerhetskontroll för Java respektive Caml. Dessutom, Jif/Split (Zdancewic et al., 2002; Zheng et al., 2003) och Swift (Chong et al., 2009) automatiskt partitionera distribuerade program till lokal kod, var och en kör på en given säkerhetsnivå, som representerar den nivå av förtroende som beviljas varje värd i ett distribuerat system. Som kan förväntas, programpartitionering misslyckas när ingen värd är tillräckligt betrodd för att köra vissa delar av beräkningen, såsom kod som fungerar på hemligheter som tillhandahålls av ömsesidigt misstänkta parter. Kryptografiskt blindade utvärderingsmetoder (Diffie och Hellman, 1976) kan ibland lösa detta problem, men med en hög prestanda overhead. I stället förlitar vi oss systematiskt på säker hårdvara till praktiskt taget "boot" kortlivade, betrodda miljöer för verkställande av privilegierad kod. Exempel: ansökan om lån. Tänk på ett program som omfattar två parter, en bank som erbjuder lån och en kund som vill ansöka om ett lån utan att lämna ut privata uppgifter (åtminstone tills lånet beviljas). Antag också att banken inte vill lämna ut de parametrar som används för att utvärdera låneansökningar. Även om kunden och banken inte litar på varandra, kan de komma överens om att säkert köra lånevärderingskoden på en TPM-aktiverad klient maskin. Denna enkla beräkning beskrivs nedan. Banken skickar sin (krypterad, signerad) hemliga indata (x b ) till kunden; klienten vidarebefordrar den till koden som kör låneutvärderingen, tillsammans med sin egen indata (y c ), med hjälp av delat lokalt minne; efter säker uppstart, den TPM-skyddade koden dekryptera sin indata, utvärderar lånet, och returnerar sina resultat; slutligen, klienten får sitt resultat (y c ) och kan vidarebefordra (krypterad, signerad) utdata (x b ) till banken om lånet beviljas. De meddelanden som skickas mellan banken och TPM-skyddad kod måste vara kryptografiskt skyddade, så att till exempel bankinmatningen kan läsas och behandlas endast av denna kod-inte av kunden eller nätverket. Den kod som skyddas av TPM är kort men komplex när det gäller informationsflöden: inflödena är godkända (som låter kunden acceptera inputen från banken och vice versa) då outputen är avklassificerade (releases- shared memorying partiell information från klienten input till banken och vice versa). Dessutom måste denna kod vägra att köra flera låneutvärderingar för olika kundindata utan bankens samtycke, eftersom detta kan möjliggöra uttag av bankindata. Kompilera med minimala TCBs. Vi sammanställer tvingande program med säkerhets- och lokalanmärkningar till distribuerade program med hjälp av kryptografi och TPM, och vi visar att vårt sammanställningssystem bevarar information-flöde säkerhet under standard kryptografiska antaganden. I detta syfte anger vi en delmängd av TPM-instruktionerna inom ett centralt nödvändigt programmeringsspråk. Vår modell syftar till formell enkelhet samtidigt som den återspeglar de viktigaste säkerhetsdetaljerna i hårdvara och kryptografiska specifikationer, på en detaljnivå som är tillräcklig för att resonera om informationsflöden. Vi modellerar säkra instruktioner för att hantera monotona räknare; mäta kod; köra kod i isolering; kryptografiskt signera data med hjälp av den privata certifikatnyckeln av TPM; och kryptografiskt sigill och oseal data i samband med någon kod. Vi använder detta tvingande språk som mål för en ny säkerhetsbevarande kompilator, byggd genom att anpassa och utvidga det senaste arbetet med kryptografiskt stöd för att genomdriva informationsflödespolicyer (Fournet och Rezk, 2008; Fournet et al., 2009). I sitt arbete är tvingande kommandon kommenterade med en värdplats, som anger var kommandot ska köras. Varje plats ges också en säkerhetsnivå, som används för att skriva källkodsprogrammet. Deras kompilator, CFLOW, genererar ett protokoll för att säkra överföringen av kontroll mellan platser, som anges av styrflödet i källkodsprogrammet, och selektiv kryptering och autentisering för att säkra utbytet av data. Vi lägger till stöd för dynamisk kodlänkning och ett mer efterlåtet typsystem, vilket gör det möjligt för oss att sammanställa källkodsprogram som utför nästan godtyckliga avklassificeringar och supporter. Vi tillhandahåller också stöd för att implementera betrodda platser genom att förlita oss på säkra instruktioner på relativt mindre pålitliga maskiner. Därför får vi distribuerade system som består av vanlig applikationskod och privilegierad kod, med anpassat kryptografiskt stöd för att samordna deras utförande, så att alla informationsflöde egenskaper hos källkodsprogrammet bevaras. Sammanfattningsvis är våra viktigaste bidrag: 1. En operationell semantik för modellering av TPM-baserad säkerhet, med fokus på TCB-reduktion genom högre orderprogrammering, med provkod och säkerhetsegenskaper. 2. Utgångspunkten är följande: En robust, flexibel förlängning av CFLOW, vilket möjliggör godkännande och avklassificering i maskinskrivna källkodsprogram, med förbättrade säkerhetsdefinitioner och teorem. 3. Vad är det som händer? Ett samlingsschema för att starta betrodda värdar på begäran, dra nytta av TPM-intyg, med korrekthet och säkerhet teorem. Innehåll. I avsnitt 2 definieras ett absolut nödvändigt, probabilistiskt, högordnat programmeringsspråk. I avsnitt 3 definieras informationsflödespolicyer, aktiva motståndare och målsäkerhetsegenskaper. Avsnitt 4 beskriver och formaliserar säkra hårdvaruinstruktioner. I avsnitt 5 presenteras CFLOW-kompilatorn och dess teorem. Avsnitt 6 visar hur man använder TPM-funktioner för att implementera säkra virtuella värdar, såsom de som produceras av CFLOW. Ett utvidgat papper, CFLOW-kompilatorn och olika kodprover finns tillgängliga på http://msr-inria.inria.fr/projects/sec/cflow. Den utökade tidningen presenterar ytterligare material, inklusive bevis, experimentella resultat som erhållits genom att anpassa CFLOW för att generera statiskt kopplade C-kod och köra den på flera små virtuella maskiner; diskussioner om vår delade minnesmodell och schemaläggning; och ytterligare resultat på testade startsekvenser när motståndaren kan schemalägga, starta om och korrupta värdmaskiner (men inte deras TPMs).
REF presenterar en säker kompilator för att översätta program och policyer till kryptografiska implementationer, fördelade på flera maskiner utrustade med TPMs.
Compiling Information-Flow Security to Minimal Trusted Computing Bases
{'venue': 'ESOP', 'journal': None, 'mag_field_of_study': ['Computer Science']}