Safety enforcement via programmable strategies in Maude

Abstract

[ES] El objetivo de este trabajo es formalizar un mecanismo general para garantizar la seguridad de las computaciones en lógica de reescritura. La técnica propuesta consiste en una transformación de programas que garantiza que el sistema transformado satisface los invariantes de seguridad definidos por el usuario, evitando así que el sistema alcance estados considerados inseguros. La transformación es genérica y no depende de estrategias ad-hoc, sino que éstas se definen como aserciones que se traducen de forma automática al lenguaje de estrategias de Maude, recientemente definido. La técnica propuesta se ha implementado en una herramienta llamada STRASS y su eficiencia y escalabilidad se han evaluado empíricamente con excelentes resultados que demuestran su viabilidad en la práctica.

[EN] This work aims to formalize a general mechanism for safety enforcement in rewriting logic computations. The proposed technique consists of a program transformation that guarantees that the transformed system satisfies user-defined invariants, thus preventing the system from reaching states considered insecure. The transformation is generic and does not depend on ad-hoc strategies but relies on the newly defined Maude strategy language. The proposed technique has been implemented in a tool called STRASS and its efficiency and scalability have been empirically evaluated with excellent results which demonstrate that the technique pays off in practice.