© 2020 IIETA. This article is published by IIETA and is licensed under the CC BY 4.0 license (http://creativecommons.org/licenses/by/4.0/).
OPEN ACCESS
Railway interlocking systems (RIS) are responsible for the control of trains’ movements by allowing or denying their routing according to safety rules. Originally built as mechanical systems then as electrical mechanical systems, they are modelled as relay-based electrical circuit diagrams and checked manually. Even recent computer based RIS are still modelled as relay diagrams. Manual checking of safety in such a critical context is an issue that needs to be addressed by the railway domain. In this context, one of the objectives of the LCHIP project is the development of computer-based RIS based on the formal specification of the RIS behaviour, which allows the generation of formally checked computer binaries by refinement. However, the produced binaries may be accessed and tampered with by ill-intended persons as computer code is easier to analyse and understand than electrical mechanical systems. In the context of the LCHIP project, binaries are run on a Microchip PIC32 MCU embedding two independent 32-bit MIPS processors. The choice of such generic architecture allows easier production and maintainability, lower production costs and easier replacement in case of hardware failure. It also makes it easier to reverse engineer compiled software as the MIPS architecture is well documented and has a small instruction set. This paper presents how binaries can be obtained using the B-method formal language and it discusses the usage of software obfuscation as a way to ensure security of these binaries. Obfuscation transforms a piece of software to make it impossible to understand for potential attackers, while keeping its observable behaviour: obfuscated software give the same outputs for the same inputs as their unobfuscated counterparts. As the obfuscation transformations do not alter the behaviour of formally checked generated binaries in a way that would void the safety checking, it is possible to secure computer based RIS and prevent ill-intended persons from tampering with them.
code obfuscation, formal methods, railway interlocking systems, safety, security
[1] Hansen, K.M., Formalising railway interlocking systems. Nordic Seminar on Dependable Computing Systems, Citeseer, pp. 83–94, 1998.
[2] Haxthausen, A.E., Le Bliguet, M. & Kjær, A.A., Modelling and verification of relay interlocking systems. Monterey Workshop, Springer, pp. 141–153, 2008.
[3] Akita, K., Watanabe, T., Nakamura, H. & Okumura, I., Computerized interlocking system for railway signaling control: smile. IEEE Transactions on Industry Applications, (3), pp. 826–834, 1985.
[4] Abrial, J.R., The B-Book: Assigning Programs to Meanings. Cambridge University Press: New York and NY and USA, 1996.
[5] Behm, P., Benoit, P., Faivre, A. & Meynadier, J.M., Meteor: a successful application of b in a large project. International Symposium on Formal Methods, Springer, pp. 369–387, 1999.
[6] Lecomte, T., Servat, T., Pouzancre, G. et al., Formal methods in safety-critical railway systems. 10th Brasilian Symposium on Formal Methods, pp. 29–31, 2007.
[7] Guiho, G. & Hennebert, C., Sacem software validation. Software Engineering, 1990. Proceedings., 12th International Conference on, IEEE, pp. 186–191, 1990.
[8] Theeg, G., Railway signalling & interlocking international compendium. PMC Media House GmbH: BingenHamburg, 2017.
[9] Rétiveau, R., La signalisation ferroviaire. Presse de l’école nationale des Ponts et Chaussées, 1987.
[10] de Almeida Pereira, D.I., Deharbe, D., Perin, M. & Bon, P., B-specification of relaybased railway interlocking systems based on the propositional logic of the system state evolution. International Conference on Reliability, Safety, and Security of Railway Systems, Springer, pp. 242–258, 2019.
[11] Fantechi, A., Fokkink, W. & Morzenti, A., B-specification of relay-based railway interlocking systems based on the propositional logic of the system state evolution. Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 61–84, 2013.
[12] Schneider, S., The B-Method: An Introduction. Palgrave, 2001.
[13] Leuschel, M. & Butler, M., Prob: a model checker for b. International Symposium of Formal Methods Europe, Springer, pp. 855–874, 2003.
[14] ClearSy, Atelier B User Manual, version 4.0. ClearSy System Engineering, Parc de la Duranne – 320 av. Archimède – Les Pléïades III Bat A – 13857 AIX EN PROVENCE CEDEX 3 – FRANCE.
[15] Sekerinski, E. & Sere, K., Program Development by Refinement: Case Studies Using the B Method. Springer Science & Business Media, 2012.
[16] Burdy, L. & Meynadier, J.M., Automatic refinement. Proceedings of BUGM at FM, 99, 1999.
[17] Collberg, C., Thomborson, C. & Low, D., A taxonomy of obfuscating transformations. http://wwwcsaucklandacnz/staff-cgi-bin/mjd/csTRcgipl?serial, 1997.
[18] Collberg, C. & Nagra, J., Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley Professional, 1st edition, 2009.
[19] Harrison, W. & Kenneth, M., A complexity measure based on nesting level. ACM SIGPLAN Notices, 16, pp. 63–74, 1981.
[20] Appel, A., Deobfuscation is in np, 2002.
[21] Collberg, C.S. & Thomborson, C., Watermarking, tamper-proofing, and obfuscation – tools for software protection. IEEE Transactions on Software Engineering, 28(8), pp. 735–746, 2002.
[22] Aucsmith, D., Tamper resistant software: an implementation. Information Hiding, ed. R. Anderson, Springer Berlin Heidelberg: Berlin, Heidelberg, pp. 317–333, 1996.
[23] Wang, X. & Yu, H., How to break md5 and other hash functions. Advances in Cryptology – EUROCRYPT 2005, ed. R. Cramer, Springer Berlin Heidelberg: Berlin, Heidelberg, pp. 19–35, 2005.