Towards Security Assurance in Round-Trip Engineering: A Type-Based Approach

作     者：Pavlich-Mariscal, Jaime A. Consuelo Franky, Maria Lopez, Ariel 

作者机构：Pontificia Univ Javeriana Dept Ingn Sistemas Bogota Colombia Univ Catolica Norte Dept Ingn Sistemas & Comput Antofagasta Chile 

出 版 物：《ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE》 (理论计算机科学电子札记)

年 卷 期：2013年第292卷

页      面：83-94页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Pontificia Universidad Javeriana and Banco Santander S.A 

主　　题：Model-Driven Software Engineering Round-Trip Engineering Security Assurance Access Control 

摘      要：Security assurance is a property that ensures that the application code behaves consistently with the access control policy specified at the design level. Security assurance proofs are valid as long as software engineers do not modify the generated code. This assumption does not hold in Round-Trip Engineering, since programmers may modify the generated code and the models are automatically re-generated. This paper proposes a round-trip engineering approach for access control that preserves security assurance both when generating code from models and vice versa. The approach is to extend programming languages typing mechanisms with additional rules that ensure consistency between models and code, even when code is arbitrarily modified by programmers. This paper presents a formal description of the solution and an initial sketch of the required proofs of correctness. Ongoing work is the development of a prototype to automate most of the process and its validation in a case study.