scholarly journals cake_lpr: Verified Propagation Redundancy Checking in CakeML

2021 ◽  
pp. 223-241
Author(s):  
Yong Kiam Tan ◽  
Marijn J. H. Heule ◽  
Magnus O. Myreen
Keyword(s):  
Binary Code ◽  
State Of The Art ◽  
Trusted Computing ◽  
Proof System ◽  
Efficiency Gains ◽  
Machine Code ◽  
Proof Validation ◽  
Proof Checker ◽  
Trusted Computing Base ◽  
Checkable Proof

AbstractModern SAT solvers can emit independently checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is propagation redundancy (PR). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This paper describes the first approach to formally verify PR proofs on a succinct representation; we present (i) a new Linear PR (LPR) proof format, (ii) a tool to efficiently convert PR proofs into LPR format, and (iii) , a verified LPR proof checker developed in CakeML. The LPR format is backwards compatible with the existing LRAT format, but extends the latter with support for the addition of PR clauses. Moreover, is verified using CakeML ’s binary code extraction toolchain, which yields correctness guarantees for its machine code (binary) implementation. This further distinguishes our clausal proof checker from existing ones because unverified extraction and compilation tools are removed from its trusted computing base. We experimentally show that LPR provides efficiency gains over existing proof formats and that the strong correctness guarantees are obtained without significant sacrifice in the performance of the verified executable.

scholarly journals Threats and Vulnerabilities to IoT End Devices Architecture and suggested remedies

2020 ◽  
Vol 8 (6) ◽  
pp. 5712-5718
Keyword(s):  
Decision Making ◽  
Internet Of Things ◽  
Data Processing ◽  
Trusted Computing ◽  
External World ◽  
Security Threats ◽  
Iot Applications ◽  
Trusted Computing Base ◽  
Chain Of Trust ◽  
New Challenges

Due to decentralization of Internet of Things(IoT) applications and anything, anytime, anywhere connectivity has increased burden of data processing and decision making at IoT end devices. This overhead initiated new bugs and vulnerabilities thus security threats are emerging and presenting new challenges on these end devices. IoT End Devices rely on Trusted Execution Environments (TEEs) by implementing Root of trust (RoT) as soon as power is on thus forming Chain of trust (CoT) to ensure authenticity, integrity and confidentiality of every bit and byte of Trusted Computing Base (TCB) but due to un-trusted external world connectivity and security flaws such as Spectre and meltdown vulnerabilities present in the TCB of TEE has made CoT unstable and whole TEE are being misutilized. This paper suggests remedial solutions for the threats arising due to bugs and vulnerabilities present in the different components of TCB so as to ensure the stable CoT resulting into robust TEE.

scholarly journals ALMA versus DDD

2008 ◽  
Vol 5 (2) ◽  
pp. 119-136
Author(s):  
Cruz da ◽  
Pedro Henriques ◽  
Maria Pereira
Keyword(s):  
No Value ◽  
Binary Code ◽  
Main Idea ◽  
Value Added ◽  
Program Comprehension ◽  
Conceptual Level ◽  
Machine Code ◽  
Abstract Representation ◽  
Source Program

To be a debugger is a good thing! Since the very beginning of the programming activity, debuggers are the most important and widely used tools after editors and compilers; we completely recognize their importance for software development and testing. Debuggers work at machine level, after the compilation of the source program; they deal with assembly, or binary-code, and are mainly data structure inspectors. ALMA is a program animator based on its abstract representation. The main idea is to show the algorithm being implemented by the program, independently from the language used to implement it. To say that ALMA is a debugger, with no value added, is not true! ALMA is a source code inspector but it deals with programming concepts instead of machine code. This makes possible to understand the source program at a conceptual level, and not only to fix run time errors. In this paper we compare our visualizer/animator system, ALMA, with one of the most well-known and used debuggers, the graphical version of GDB, the DDD program. The aim of the paper is twofold: the immediate objective is to prove that ALMA provides new features that are not usually offered by debuggers; the main contribution is to recall the concepts of debugger and animator, and clarify the role of both tools in the field of program understanding, or program comprehension. .

scholarly journals Composite Enclaves: Towards Disaggregated Trusted Execution

2021 ◽  
pp. 630-656
Author(s):  
Moritz Schneider ◽  
Aritra Dhar ◽  
Ivan Puddu ◽  
Kari Kostiainen ◽  
Srdjan Čapkun
Keyword(s):  
Case Studies ◽  
Large Scale ◽  
Trusted Computing ◽  
Design Time ◽  
Wide Range ◽  
Trusted Computing Base ◽  
Recent Developments ◽  
Configurable Hardware ◽  
Low Performance ◽  
Specialized Hardware

The ever-rising computation demand is forcing the move from the CPU to heterogeneous specialized hardware, which is readily available across modern datacenters through disaggregated infrastructure. On the other hand, trusted execution environments (TEEs), one of the most promising recent developments in hardware security, can only protect code confined in the CPU, limiting TEEs’ potential and applicability to a handful of applications. We observe that the TEEs’ hardware trusted computing base (TCB) is fixed at design time, which in practice leads to using untrusted software to employ peripherals in TEEs. Based on this observation, we propose composite enclaves with a configurable hardware and software TCB, allowing enclaves access to multiple computing and IO resources. Finally, we present two case studies of composite enclaves: i) an FPGA platform based on RISC-V Keystone connected to emulated peripherals and sensors, and ii) a large-scale accelerator. These case studies showcase a flexible but small TCB (2.5 KLoC for IO peripherals and drivers), with a low-performance overhead (only around 220 additional cycles for a context switch), thus demonstrating the feasibility of our approach and showing that it can work with a wide range of specialized hardware.

scholarly journals Formal Verification of a Mandatory Integrity Control Model for the KasperskyOS Operating System

2020 ◽  
Vol 32 (6) ◽  
pp. 31-48
Author(s):  
Vladimir Sergeevich Burenkov
Keyword(s):  
Operating System ◽  
Formal Verification ◽  
Operating Systems ◽  
Trusted Computing ◽  
Control Model ◽  
Discrete Mathematics ◽  
Active Components ◽  
Access To Resources ◽  
Trusted Computing Base ◽  
Automated Proof

Models of mandatory integrity control in operating systems usually restrict accesses of active components of a system to passive ones and represent the accesses directly. This is suitable in case of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, due to the sheer complexity of such components, it is extremely nontrivial to prove such a model to be adequate to the real system. KasperskyOS is a microkernel operating system that organizes access to resources via components that are not necessarily part of the trusted computing base. KasperskyOS implements a specifically developed mandatory integrity control model that takes such components into account. This paper formalizes the model and describes the process of automated proof of the model’s properties. For formalization, we use the Event-B language. We clarify parts specific to Event-B to make our presentation accessible to professionals familiar with discrete mathematics but not necessarily with Event-B. We reflect on the proof experience obtained in the Rodin platform.

Sign in / Sign up

Export Citation Format

Share Document