Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of Hardware Peripheral with Security Property
KTH, School of Computer Science and Communication (CSC).
KTH, School of Computer Science and Communication (CSC).
2017 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesisAlternative title
Formell verifikation av extern hårdvara med säkerhetskrav (Swedish)
Abstract [en]

One problem with computers is that the operating system automatically trusts any externallyconnected peripheral. This can result in abuse when a peripheral technically can violate the security model because the peripheral is trusted. Because of that the security is an important issue to look at.The aim of our project is to see in which cases hardware peripherals can be trusted. We built amodel of the universal asynchronous transmitter/receiver (UART), a model of the main memory(RAM) and a model of a DMA controller. We analysed interaction between hardware peripherals,user processes and the main memory.One of our results is that connections with hardware peripherals are secure if the hardware is properly configured. A threat scenario could be an eavesdropper or man-in-the-middle trying to steal data or change a cryptographic key.We consider the use-cases of DMA and protecting a cryptographic key. We prove the well-behavior of the algorithm. Some error-traces resulted from incorrect modelling that was resolved by adjusting the models. Benchmarks were done for different memory sizes.The result is that a peripheral can be trusted provided a configuration is done. Our models consist of finite state machines and their corresponding SMV modules. The models represent computer hardware with DMA. We verified the SMV models using the model checkers NuSMV and nuXmv.

Abstract [sv]

Målet med vårt projekt är att verifiera olika specifikationer av externa enheter som ansluts till datorn. Vi utför formell verifikation av sådan datorutrustning och virtuellt minne. Verifikation med temporal logik, LTL, utförs. Specifikt verifierar vi 4 olika use-case och 9 formler för seriell datakommunikation, DMA och virtuellt minne. Slutsatsen är att anslutning av extern hårdvara är säker om den är ordentligt konfigurerad.Vi gör jämförelser mellan olika minnesstorlekar och mätte tidsåtgången för att verifiera olika system. Vi ser att tidsåtgången för verifikation är långsammare än linjärt beroende och att relativt små system tar relativt lång tid att verifiera.

Place, publisher, year, edition, pages
2017. , 34 p.
Keyword [en]
Formal Verification NuSMV JavaPathFinder Spin/Promela CTL LTL DMA UART Model Checking Theorem Proving
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-209807OAI: oai:DiVA.org:kth-209807DiVA: diva2:1114579
Presentation
2017-06-01, E51, Osquars backe 14, Campus KTH, 13:15 (English)
Supervisors
Examiners
Available from: 2017-06-24 Created: 2017-06-24 Last updated: 2017-06-27Bibliographically approved

Open Access in DiVA

fulltext(743 kB)43 downloads
File information
File name FULLTEXT01.pdfFile size 743 kBChecksum SHA-512
f886919da73b4a4088e6242c9a05a8fb6948a8d203b8481519cc7ea77a36466ef9161bade1f1ca0f55521b638f8084df5a7c18ca9cddaa0e8d64ca6aa4c062c0
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Yao Håkansson, JonathanRosencrantz, Niklas
By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 43 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 812 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf