Who actually has control over your systems?
For critical or sensitive applications most standard software is unsuitable. On the one hand, vulnerabilities allow attackers to gain control, on the other hand, security updates entail adjustments and downtime. Our component-based platform enables robust systems where critical software is protected by formally proven components.
Industrial control systems often have a lifetime of several decades. At the same time Industry 4.0 and IoT brings the Internet and networked IT to this domain. Security holes and monthly patch cycles are the rule here.
By combining trusted, formally verified filter components with execution environments for legacy software the Componolit platform enables trustworthy operation of industrial applications.
Smartphones are as vulnerable as they are useful. The next careless click may result in the loss of confidential data, financial damage or attacks on other devices. The reason are archaic system architectures and development methods in the light of ever more complex requirements.
The Componolit platform offers maximum security to end users without restricting the usability of their devices.
Due to the vast number of functional requirements, software is constantly getting bigger and more complex. This increases the likelihood of exploitable vulnerabilities. Attacks on one part can spread to another, critical part because of the monolithic architecture of our current systems.
The Componolit platform relies on a component-based architecture which run applications in isolation by default. Legacy software can be reused through various compatibility layers and are protected by trustworthy, formally verified components.Read on
Componolit is an owner-operated company with a strong emphasis on highly trustworthy software, component-based systems and formal verification.
Our mission is to enable our customers to create secure IT systems that are ready for a connected world. To achieve this goal we develop the Componolit open source platform. We focus on two applications: a trusted operating system for mobile devices and the security of industrial applications.
Due to the vast number of functional requirements, software is constantly getting more complex. At the same time, more devices are connected to the Internet, which increases the likelihood of exploitable vulnerabilities. Attacks on one part can spread to another critical part in current systems.
As an alternative, we build component-based architectures where applications are isolated by default. Complex software can access resources only when granted by trusted policy objects.
The correctness of these policy objects is essential for secure systems. Consequently, we provide a platform to create trustworthy formally verified components. Our environment supports different component-based platforms and is designed to be portable to new systems. We offer libraries for encryption and trusted document parsing. The interaction of trusted components can be formally modeled and there are ready-to-use security components.
Verified Components Runtime
Our runtime for the SPARK language is a downsized environment for trusted, verifiable components. Features that are too complex to implement or hard to verify have been omitted. Parts of the runtime have been formally verified to contain no runtime errors. The Genode OS Framework, the Muen Separation Kernel and Linux are supported platforms. Due to its small size and a well-defined platform interface it can be adapted to other systems easily.
Platform-Independent Verifiable Components
When creating trusted components a recurring question is how to structure them to be efficient and verifiable, especially when different component-based platforms have to be supported. Our Component Interfaces library provides a system abstraction to build SPARK applications against a common API. Components using this interface are completely asynchronous and can be compiled to the Genode OS Framework, the Muen Separation Kernel and Linux without modification.
Verified Crypto Primitives
Encryption is a common operation for trusted components and a critical function must be implemented correctly. libsparkcrypto is a formally verified implementation of several widely used cryptographic algorithms in the SPARK programming language. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.
Trustworthy Data Interchange and Validation
Processing and sanitizing untrusted data is an important and critical task for trusted components. Our JWX library can be used to handle standard JSON from unreliable sources. It is implemented in the SPARK programming language and has been proven to contain no runtime errors. In addition to JSON, it supports Base64 and JSON Web Signatures, JSON Web Keys and JSON Web Tokens to validate the origin of JSON data.
Verified XML Document Handling
XML-based formats have become a default choice in many domains. To handle XML documents in trusted components and to use it as a configuration format, we created the SXML library. It is implemented in SPARK and the absence of runtime errors and bounded stack usage have been proven. The library can be used to declare XML documents inline, parse XML text, serialize to XML and query the content of an XML tree.
Verifiable Binary Parsers
The majority of communication protocols require parsing of binary messages. Parsers routinely have security vulnerabilities due to the complexity of protocols and the ambiguity of specifications. RecordFlux is a language and toolset to formalize message formats and generate verifiable parsers for SPARK programs. It has been used to formalize the TLS 1.3 message format and will be extended to support dynamic protocol semantics in the future.
Trusted Mandatory TLS Encryption
The Transport Layer Security (TLS) protocol is arguably the most important security protocol in use today. Whenever we're using a banking app, buy goods online or send messages to friends, the connection between our device and a remote server is secured with TLS.
Despite its importance, security vulnerabilities are regularly found in TLS libraries. Many applications use those libraries in insecure ways or fail to use TLS at all. The reasons are unsafe programming languages, complex informal standards and complicated APIs.
GreenTLS is an ongoing research project to create a component-based implementation of TLS 1.3. In our architecture, security critical portions of TLS run in formally verified, isolated components. Furthermore, we formalize the TLS protocol using our RecordFlux toolset and show that the application-facing APIs can only be used in a safe manner.
Koenigsbruecker Strasse 124
Responsible for the content of this website under §55 Abs. 2 RStV
Koenigsbruecker Strasse 124
Phone: +49 351 417241990
Phone: +49 351 417241990
Based in Dresden
VAT Identification Number