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 onTrustworthy 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
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.
Technical Foundation
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.
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.
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.
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.
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.
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.
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.
Imprint
Componolit GmbH
Koenigsbruecker Strasse 124
01099 Dresden
Germany
Managing Directors
Cyrille Comar, 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