HENSOLDT Cyber succeeds in the formal verification of a first component of the TRENTOS operating system

Dr Jaap Boender, Formal Verification Engineer at HENSOLDT Cyber, succeeds in the formal verification of a first component of the TRENTOS® operating system, the keystore, and thereby sets a benchmark.

The keystore was formally verified as the first component of the HENSOLDT cyber operating system TRENTOS®. Photo: HENSOLDT Cyber GmbH

Taufkirchen/Germany, March 18th 2021 – HENSOLDT Cyber makes a unique breakthrough in a little-known yet very important area of formal verification. Formal verification is the process of proving the correctness of a system with respect to a particular formal specification or property using formal methods of mathematics.

Dr Jaap Boender, Formal Verification Engineer at HENSOLDT Cyber, has, after a good year and a half of demanding work, managed to formally verify a first component of the new high-security operating system TRENTOS® (Trusted Entity Operating System).

This achievement now paves the way for the future formal verification of other larger and more complex components. Dr Jaap Boender, with the support of his colleague Goran Badevic and scientific advice from HENSOLDT Cyber Chief Scientist Prof. Dr Gernot Heiser, will now tackle further components.

“Formal verification on an industrial scale is still a relatively under-researched area and therefore it is special that HENSOLDT Cyber is researching in it. The seL4 microkernel on which our TRENTOS operating system is based has already been formally verified, and in the future it is conceivable to increasingly automate formal verification and thus verify more complex systems. The first project, however, is our keystore,” explains Dr Boender.

Further information at https://hensoldt-cyber.com/2021/03/16/formal-verification-keystore/

About HENSOLDT Cyber

Founded in 2018, HENSOLDT Cyber GmbH is a German Corporate Start-up company based in Taufkirchen near Munich that develops embedded information technology products meeting the highest security requirements. These integrate a highly secure operating system with security hardened hardware, thus creating a secure IT instead of IT security for the global IT market. The company combines more than 50 years of experience in defence and security electronics of the HENSOLDT Group with academic world-class expertise in hardware and software development. HENSOLDT Cyber currently employs over 50 people at various locations.

Further information about the company can be found at www.hensoldt-cyber.com

Press contact

Simone Rudow
Tel.: +49 (0) 174 218 8102
simone.rudow@hensoldt-cyber.com

Change your language

More News

First order for HENSOLDT’s in-house AI and Cyber Solutions

HENSOLDT equips undisclosed South East Asian customer with Xpeller counterdrone solution.

HENSOLDT delivers radar training system enhancement to RAAF

Delivering an enhancement to Australian Air Force’s Radar Operational Maintenance Trainer

Extended Trustworthiness through binary verification of seL4® microkernel on RISC-V® processor architecture

Taufkirchen, Germany, May 5th 2021 – German cybersecurity company HENSOLDT Cyber in partnership with CSIRO, has announced the release of an automated…