Specification and Implementation of secure web systems

信息系统在当今经济中很普遍。如今，它们广泛分布在互联网上。为了方便它们的构建、部署、维护和提高它们的可访问性，它们现在被构建为可以在互联网上从任意位置调用的Web服务。这些信息系统传递的是私人的、有价值的信息，只有经过授权的人员才能访问。金融系统和病历等多个领域都受到严格的监管，如Sarbane-Oxley，HIPAAA和PIPEDA。安全性和隐私性是使用几种技术来解决的，如身份验证、加密和安全通信协议。我们的目标是安全的另一个方面，我们称之为功能安全。它描述了业务需求级别的安全规则。例如，客户的投资账户应该只允许其经纪人及其经理人访问;病人的健康记录应该只提供给其治疗医生，或者有限的信息可以在有限的时间内提供给咨询专家。功能安全可以在不同的级别上指定：数据属性、原子服务（操作）和业务流程（原子服务的复杂排序）。该项目将：i）在这三个层次上提出了Web系统功能安全策略的规范方法; ii）定义了在面向服务的体系结构中自动实现功能安全策略的合成算法。功能安全政策将与功能要求分开规定，以便于其维护和实施。实现这些策略的安全内核将与功能需求的实现分离，从而实现在线修改安全规则，而无需修改服务的实现。我们的方法基于形式化方法，允许使用形式化验证技术来确保安全策略的一致性和充分性。

Information systems are prevalent in today's economy. Nowadays, they are intensively distributed andaccessible over the Internet. To facilitate their construction, deployment, maintenance and improve theiraccessibility, they are now constructed as web services which may be invoked over the Internet from arbitrarylocations. These information systems convey private, valuable information which must be only accessed byauthorized personnel. Several domains like financial systems and patient records are subject to strictregulations like Sarbane-Oxley, HIPAAA, and PIPEDA. Security and privacy are addressed using severaltechnology like authentication, encryption and secure communication protocols. We are targeting anotheraspect of security, which we call functional security. It describes the security rules that are at the businessrequirements level. For instance, the investment account of a customer should only be accessible to its brokerand his manager; the health record of a patient should only be available to its treating doctor or limitedinformation could be made available for a limited time period to consulting specialists. There are variouslevels at which functional security can be specified : data attributes, atomic services (actions) and businessprocess (a complex ordering of atomic services). This project will: i) propose a specification method forfunctional security policies for web systems at these three levels; ii) define synthesis algorithms toautomatically implement functional security policies into a security kernel, within the context of aservice-oriented architecture. Functional security policies will be specified separately from functionalrequirements, in order to facilitate their maintenance and implementation. The security kernel implementingthese policies will be separated from the implementation of the functional requirements, enabling onlinemodification of security rules without having to modify the implementation of the services. Our approach isbased on formal methods, enabling the use of formal verification techniques to ensure the consistency andadequacy of security policies.