Provably Forgetting of Information in Manufacturing Systems: Verification of the KASTEL Industry Demonstrator

During the manufacturing process, information are generated and aggregated that constitute a business secrets and therefore need a high protection. On the other hand, if we can prove, that an information is absented, the effort for the protection for this system could be invested on different information, aspects or systems. For this, we develop the notion of information forgetting of a reactive system. This notion describes that a reactive system needs to forget the information about a secret within a certain amount of cycles. This property limits the amount of historical information an attacker can learn by observing a manufacturing system. Moreover, we formalise and prove the notion of an information forgetting system with Relational Test Tables.
We evaluate the verification on the industry demonstrator for \textsc{kastel svi} project, which was provided by the Fraunhofer IOSB and developed by industrial third-party contractor. In this demonstrator, we are able to show, that a selected business secret – the number of wheel turns – is not forgotten. We suggest and prove a fix of the leak. We close with an elaborate discussion on the verification and results and also with remarks to the how information forgetting relates supports quantifiable security.