Matematisk logik verificerer sikkerhed i skyen

Hvad er forbindelsen mellem græske filosoffer og cloudsikkerhed? En engelsk datalogi-professor med en central rolle for Amazons cloudsikkerhed taler med Version2.

Byron Cook er professor i datalogi på University College London, hvor han forsker i, hvordan sikkerhed i software kan verificeres ved hjælp af matematisk logik. Den forskning har gjort ham til leder af Amazons Automated Reasoning Group (ARG), der arbejder med at gøre forskellige AWS-services sikre.

Automatisk ræsonnement anvender algoritmiske teknikker, der forsøger at udarbejde matematiske beviser for sikkerheden i komplekse systemer, og som enhver erfaren devops ved, så kan cloud computing-miljøer indeholde ganske megen kompleksitet. Derfor er Byron Cooks og ARG's arbejde uhyre relevant i cloudmæssig sammenhæng.

Professor Byron Cooks forskningsområde er lettere langhåret, som han selv, men han gør sit bedste for at forklare Version2, hvordan anvendelsen af matematisk logik kan anvendes til at gøre software sikker.

De gamle grækeres betydning for cloudsikkerhed

Han går tilbage til gamle grækere som Aristoteles, Euklid og Pythagoras, der etablerede fundamentet for matematisk logik for tusinder af år tilbage.

»Matematisk logik er fundamentet for viden og sandhed i vores kultur og er udviklet gennem mere end 2.000 år,« siger Byron Cook.

Der er to begreber, som er centrale for forståelsen af Byron Cooks og ARG's arbejde:

  • Et bevis er et endeligt argument, der ved hjælp af logisk ræsonnement når frem til en sandhed.

  • En læresætning er et udsagn, der er bevist at være sandt ved hjælp af et matematisk bevis.

  • Et eksempel, som de fleste kender, er Pythagoras' læresætning om retvinklede trekanter, hvor a^2 + b^2 = c^2.

Der er uendeligt mange mulige retvinklede trekanter, så det er umuligt at eftervise læresætningen ved at måle siderne i alle retvinklede trekanter, men vi ved, at sætningen gælder for alle retvinklede trekanter, fordi den er blevet eftervist ved hjælp af matematisk logik.

»Pythagoras' sætning gælder for alle retvinklede trekanter, og det var faktisk Euklid, der kom med beviset omkring år 300 f.Kr.,« siger Byron Cook, der anvender den matematisk logiske tradition fra de gamle grækere til at bevise, at et kompleks system er korrekt, ved hjælp af, hvad han og hans kollegaer kalder provable security eller bevisbar sikkerhed.

»Provable security er anvendelse af automatisk ræsonnement til at bevise, at et system har nogle ønskede egenskaber. Automatisk ræsonnement anvender algoritmer og matematisk logik til at finde beviser for korrektheden af komplekse systemer,« siger Byron Cook.

10 minutters bevis – eller test, indtil Solen brænder ud

Udfordringen ved komplekse systemer er, at de har, om ikke uendeligt mange tilstande som i tilfældet med retvinklede trekanter, så et meget stort antal tilstande, der i praksis gør det umuligt at teste dem alle.

Som eksempel nævner Byron Cook S2N, som er en open source-implementering af TLS. S2N anvendes i Amazons cloud, eksempelvis S3 og andre services.

»Antallet af tilstande i S2N er 2 opløftet i 12.000, så hvis du ønsker vise, at implementeringen er korrekt med konventionelle metoder ved at køre test af alle tilstandene, så har du brug for en million Haswell-mikroprocessorer, der kører parallelt, og det vil tage mange gange Solens levetid (Solens forventede resterende levetid er 5 milliarder år, red.) for at teste alle tilstandene,« forklarer Byron Cook.

Det er altså ikke muligt at køre alle de nødvendige tests, der gør det muligt at konkludere, at S2N ikke har nogen usikre tilstande.

»Hvad folk har gjort hidtil har været at anvende fuzzing, og de har prøvet at være smarte med deres test-cases. Hvis fuzzeren melder tilbage, at den ikke kunne finde nogen bugs, så ved du ikke, om der reelt er nogen bugs, du ved blot, at fuzzeren ikke kunne finde nogen,« siger Byron Cook.

Ved hjælp af specielle værktøjer kan det bevises, at S2N-implementeringen er korrekt. Det kan ifølge Byron Cook gøres på 10 minutter med de rette værktøjer. Du kan læse mere om detaljerne i S2N og automatisk ræsonnement her.

Alting flyder, men fornuft kan hjælpe

Amazon anvender ikke kun værktøjer med automatisk ræsonnement til at verificere korrektheden af eksempelvis S2N, men anvender dem også til at gøre det nemmere for udviklere og devops at tjekke konfiguration og compliance.

Det gælder eksempelvis Identity and Access Management (IAM) og Simple Storage Service (S3), der begge anvender Zelkova-værktøjet (PDF) til at holde øje med, om best practices i sikkerhed overholdes.

Eksempelvis anvender S3 Zelkova til at tjekke, om en uautoriseret bruger har adgang til at skrive eller læse fra en S3-bucket grundet en forkert defineret bucket policy.

Zelkova anvendes også i AWS Config, AWS Trusted Advisor, Amazon Macie, Amazon GuardDuty og AWS IoT Device Defender.

Et andet værktøj er Tiros, som anvendes af Amazon Inspector til at tjekke, om konfigurationen af netværksressourcer og adgangsrettigheder ikke uforvarende har givet adgang fra det åbne internet til, hvad der skulle være beskyttede netværksressourcer. Det lyder måske som noget, der burde være rimeligt enkelt at styre, men i komplekse cloud-miljøer er det svært at holde styr på den slags manuelt.

Ikke mindst når ’alting flyder’, for nu at citere en anden af de gamle græske filosoffer, Heraklit.

Her skal understreges, at ’alting flyder’ skal forstås som, at alting er i konstant forandring, hvilket gælder de fleste it-miljøer – ikke at alting er kaos.

Tips og korrekturforslag til denne historie sendes til tip@version2.dk
Følg forløbet
Kommentarer (5)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
Bjarne Thomsen

Kurt Gödel (med kontor ved siden af Einstein) viste, at der findes sætninger, som ikke kan bevises. Alan Turing viste nogle få år senere, at Gödels resultat betyder, at der findes algoritmer, som man ikke kan bevise vil stoppe. Hvordan sikrer Byron Cook sig, at C-programmet S2N ikke falder i Gödels og Turings fælde? Programmets navn står for øvrigt for signal-to-noise. Jeg kender ikke svaret.

  • 0
  • 0
Bjarne Thomsen

er definitionen på HMAC algoritmen. Al den floromvundne snak om Euklids geometri hentyder tilsyneladende blot til, at alle boolske operatorer kan udtrykkes ved xor. Men artiklen er ganske interessant:
[https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26]
5 Conclusion
"In this case study we have described the development and operation in practice of a continously checked proof ensuring key properties of the TLS implementation used by many Amazon and AWS services. ... , we developed a proof structure that nearly eliminates the need for developers to understand or modify the proof following modifications to the code."
Man vil altså undgå den "typiske fremgangsmåde at afvise ændringen, hvis sikkerheden ikke kan verificeres". Verifikationen sker angiveligt automatisk og kontinuert, så man undgår kostbare afbrydelser.

  • 0
  • 0
Michael Cederberg

Man vil altså undgå den "typiske fremgangsmåde at afvise ændringen, hvis sikkerheden ikke kan verificeres". Verifikationen sker angiveligt automatisk og kontinuert, så man undgår kostbare afbrydelser.

Man må håbe at verifikation af sikkerheden sker inden løsninger deployes. Eller i denne tilfælde inden en version af S2N releases. Sikkerhed er ikke noget man kigger på efter koden er kommet i produktion.

  • 0
  • 0
Log ind eller Opret konto for at kommentere