A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach
No doubt, a person of modern society relying on Embedded Systems (ESs) has increased rapidly and the era of digital machines is gaining popularity among users and also systems providers. At the same time, such instruments face substantial security challenges because they usually operate in a physica...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2019-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8910543/ |
| _version_ | 1818407644855009280 |
|---|---|
| author | Abdo Ali A. Al-Wosabi Zarina Shukur |
| author_facet | Abdo Ali A. Al-Wosabi Zarina Shukur |
| author_sort | Abdo Ali A. Al-Wosabi |
| collection | DOAJ |
| description | No doubt, a person of modern society relying on Embedded Systems (ESs) has increased rapidly and the era of digital machines is gaining popularity among users and also systems providers. At the same time, such instruments face substantial security challenges because they usually operate in a physically unprotected environment, and thus attract the attackers to gain unauthorized access for utilizing the system functions. Accordingly, system integrity is important and hence there is a need to propose a technique/tool to verify that the original/pure systems codes have been used in those devices. In this research, our main objective is to design a system architecture with a secure communication for code integrity attestation of an ES. Indeed, the study presents the proposed system architecture for ESs integrity attestation which includes two main phases: fetching an ES code at a server site and examining the ES at a remote site (using a designed user application). Essentially, the hash function (SHA-2) with a random key to calculate a unique digest value for a targeted system have been utilized. Also, the study used timestamps and nonce values, two secure keys, and public key algorithm to design a secure protocol in-order to prevent potential attacks during data and the associated values transfer between the server and the remote user application. As many researchers state that the formal methods are very precise and accurate for presenting system specifications; this study modeled and analyzed the proposed attestation protocol using the Communicating Sequential Processes (CSP) formal method approach. Besides, the Compiler for the Analysis of Security Protocols (Casper) has been used to translate the protocol description into the corresponding process algebra CSP model. Then, the researcher used the Failures Divergences Refinement (FDR) to evaluate the proposed protocol. Those formal method tools are considered as a reliable verification measurement in-order to figure-out potential flaws and correct them. Overall, the final output of checking all the defined secrecy and authentication assertions using FDR 4.2.0, and thus all the secrecy and authentication specifications defined in the developed Casper script are passed. |
| first_indexed | 2024-12-14T09:31:07Z |
| format | Article |
| id | doaj.art-9c63e94df4ac44d59d1c3e96efae0e69 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-14T09:31:07Z |
| publishDate | 2019-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-9c63e94df4ac44d59d1c3e96efae0e692022-12-21T23:08:04ZengIEEEIEEE Access2169-35362019-01-01717023817026910.1109/ACCESS.2019.29551608910543A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP ApproachAbdo Ali A. Al-Wosabi0https://orcid.org/0000-0002-3655-8140Zarina Shukur1Center for Software Technology and Management (Softam), Faculty of Information Science and Technology (FTSM), Universiti Kebangsaan Malaysia (UKM), Bangi, MalaysiaCenter for Software Technology and Management (Softam), Faculty of Information Science and Technology (FTSM), Universiti Kebangsaan Malaysia (UKM), Bangi, MalaysiaNo doubt, a person of modern society relying on Embedded Systems (ESs) has increased rapidly and the era of digital machines is gaining popularity among users and also systems providers. At the same time, such instruments face substantial security challenges because they usually operate in a physically unprotected environment, and thus attract the attackers to gain unauthorized access for utilizing the system functions. Accordingly, system integrity is important and hence there is a need to propose a technique/tool to verify that the original/pure systems codes have been used in those devices. In this research, our main objective is to design a system architecture with a secure communication for code integrity attestation of an ES. Indeed, the study presents the proposed system architecture for ESs integrity attestation which includes two main phases: fetching an ES code at a server site and examining the ES at a remote site (using a designed user application). Essentially, the hash function (SHA-2) with a random key to calculate a unique digest value for a targeted system have been utilized. Also, the study used timestamps and nonce values, two secure keys, and public key algorithm to design a secure protocol in-order to prevent potential attacks during data and the associated values transfer between the server and the remote user application. As many researchers state that the formal methods are very precise and accurate for presenting system specifications; this study modeled and analyzed the proposed attestation protocol using the Communicating Sequential Processes (CSP) formal method approach. Besides, the Compiler for the Analysis of Security Protocols (Casper) has been used to translate the protocol description into the corresponding process algebra CSP model. Then, the researcher used the Failures Divergences Refinement (FDR) to evaluate the proposed protocol. Those formal method tools are considered as a reliable verification measurement in-order to figure-out potential flaws and correct them. Overall, the final output of checking all the defined secrecy and authentication assertions using FDR 4.2.0, and thus all the secrecy and authentication specifications defined in the developed Casper script are passed.https://ieeexplore.ieee.org/document/8910543/Embedded systemscode integritycode integrity attestationsoftware tamperingtampering detectionCSP formal method approach |
| spellingShingle | Abdo Ali A. Al-Wosabi Zarina Shukur A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach IEEE Access Embedded systems code integrity code integrity attestation software tampering tampering detection CSP formal method approach |
| title | A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach |
| title_full | A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach |
| title_fullStr | A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach |
| title_full_unstemmed | A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach |
| title_short | A Secure Protocol for Remote-Code Integrity Attestation of Embedded Systems: The CSP Approach |
| title_sort | secure protocol for remote code integrity attestation of embedded systems the csp approach |
| topic | Embedded systems code integrity code integrity attestation software tampering tampering detection CSP formal method approach |
| url | https://ieeexplore.ieee.org/document/8910543/ |
| work_keys_str_mv | AT abdoaliaalwosabi asecureprotocolforremotecodeintegrityattestationofembeddedsystemsthecspapproach AT zarinashukur asecureprotocolforremotecodeintegrityattestationofembeddedsystemsthecspapproach AT abdoaliaalwosabi secureprotocolforremotecodeintegrityattestationofembeddedsystemsthecspapproach AT zarinashukur secureprotocolforremotecodeintegrityattestationofembeddedsystemsthecspapproach |