Company RecordFlux Trustworthy Components Contact
padlock with conductor lines

Smart needs Security

Smart technologies and IoT disrupt whole industries and greatly improve efficiency, flexibility and automation. But the enhanced connectivity comes with an increased attack surface and makes systems attractive targets for cyber criminals.

We provide tools to formally model the communication of connected software and to create provably correct security components for such systems.

RecordFlux

Most communication performed by software components requires parsing of binary data. Due to the complexity of binary protocols and the ambiguity of their specifications binary parsers routinely have critical security vulnerabilities.

RecordFlux is a language and toolset for secure handling of binary formats. Formal specifications can be used for rapid prototyping in Python and to generate provably correct binary parsers and generators.

Read on

Trustworthy Security Components

Due to the vast number of functional requirements, software is constantly getting more complex which increases the likelihood of exploitable vulnerabilities. At the same time, the monolithic architecture of our current systems is inadequate to contain attacks.

The solution is to move security critical functionality into separate components and ensure they are capable of protecting the rest of the system. Our component environment enables formally verified security components with well-defined interfaces.

Read on
light bulb

About us

Componolit is a highly specialized company with a strong emphasis on 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.

The components, libraries and tools developed by Componolit are available as open source software under the GNU Affero General Public License which allow their use in free software projects. In addition, we offer commercial support, consulting and licensing. Please contact sales@componolit.com.

Communication Protocols as an Attack Vector

Security issues are common in parsers of communication protocol implementations, and new vulnerabilities are found every day. Vulnerabilities caused by incorrect parsing exist on all protocol layers: from physical and network layer protocols like Bluetooth (BlueBorne) over session-layer protocols like TLS (Heartbleed) to application-layer protocols like SMB (EternalBlue).

Communication protocols are an increasingly worthwhile attack target, as more and more devices get connected to the Internet. Their reliability is essential in business-critical, mission-critical and safety-critical software.

Imprecise Specifications and Unsafe Languages

Message formats of protocols are often complex and rarely defined precisely. Specifications commonly use a simple syntax which only captures the basic structure of messages. Additional properties, conditions, and relations between fields are often just described in English prose.

Informal descriptions are often ambiguous, inconsistent and can easily be misunderstood by developers which routinely leads to implementation bugs. The lack of a formal specification also makes automatic checks at the specification level and formal verification of implementations infeasible. Lastly, the widespread use of unsafe programming languages like C and C++ for message parsers makes critical vulnerabilities even more likely.

RecordFlux: Formal Specifications and Verifiable Code

RecordFlux is our toolset and specification language to formalize real-world binary protocols. Its specifications are powerful enough to precisely define the expected format of message fields, their constraints and the relation between different parts of messages. The correctness of a message specification is formally verified to contain no problematic constructs like an ambiguous or contradicting layout. This helps avoiding dangerous implementation errors even before writing the first line of application code.

From RecordFlux models code is generated in the SPARK programming language which is designed for high-reliability applications. SPARK programs can be proven to contain no errors like buffer overflows, use-after-free or range violations which normally result in severe security or safety issues. Using a compiled language with an adaptable runtime, RecordFlux is suitable for resource-constraint sensor devices, hardware-security modules, trusted execution environments, protocol stacks and more. Our verified component environment allows for the integration of the generated software into different types of systems.

Get the RecordFlux source code on GitHub

Technical Foundation

graph representation of TLV message

In RecordFlux, messages are encoded as directed, acyclic graph with the start of a message represented by a single initial node and the end represented by a single final node. As the layout, size, length and even presence of a field may depend on the value, size or position of other fields, the edges of the graph carry a validity condition, a size and a start position for each field.

A message is only accepted by the parser if a path from the initial node to the final node exists for which all conditions and constraints are fulfilled. The same graph structure is encoded in pre-conditions and invariants of the generated SPARK code to ensure the model is satisfied at runtime.

More details can be found in the RecordFlux research paper (paper, preprint).

RecordFlux Use-case: Trustworthy TLS Encryption

The Transport Layer Security (TLS) protocol is arguably the most important security protocol in use today. Whenever we are 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.

EU-EFRE-ESF logo

Trustworthy Security Components

Due to the vast number of functional requirements, software is constantly getting more complex which increases the likelihood of exploitable vulnerabilities. At the same time, the monolithic architecture of our current systems is inadequate to contain attacks.

The solution is to move security critical functionality into separate components and ensure they are capable of protecting the rest of the system. Our component environment enables formally verified components with well-defined interfaces.

abstract components and documents

Gneiss: Verified Platform-Independent Components

When creating trusted components a recurring question is how to structure them to be efficient and verifiable, especially when different 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 run on Linux or Genode without modification.

Get the Gneiss source code on GitHub

cloud

JWX: 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.

Get the JWX source code on GitHub

SPARK Runtime: Minimal Verified Components

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. It is available for Linux, Genode and the Muen Separation Kernel. As bare-metal targets embedded SoCs like the ESP8266, the nRF52 and the STM32F0 are supported. Due to its small size and a well-defined platform interface it can be adapted to other targets easily.

Get the Runtime source code on GitHub

SXML: 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 provide 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.

Get the SXML source code on GitHub

key ring

libsparkcrypto: 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.

Get the libsparkcrypto source code on GitHub

Imprint

Componolit GmbH
Koenigsbruecker Strasse 124
01099 Dresden
Germany

Managing Director

Alexander Senier

Responsible for the content of this website under ยง55 Abs. 2 RStV

Alexander Senier
Koenigsbruecker Strasse 124
01099 Dresden
Germany

Phone: +49 351 417241990
E-Mail: webmaster@componolit.com

Contact

Phone: +49 351 417241990
E-Mail: contact@componolit.com

Company Registration

Amtsgericht Dresden
HRB 36670
Based in Dresden

VAT Identification Number

DE312113634