@inproceedings{bytschkow2014, author = {Bytschkow, Denis and Quilbeuf, Jean and Igna, Georgeta and Rue{\ss}, Harald}, title = {Distributed MILS architectural approach for secure smart grids}, booktitle = {Smart Grid Security}, publisher = {Springer International Publishing}, pages = {16--29}, year = {2014}, month = aug, abstract = {Successful decentralized and prosumer-based smart grids need to be at least as dependable and secure as the prevailing one-way, generation-transmission-distribution-consumer power grids. With this motivation in mind, we propose a two-phase model-based design methodology for secure architectural design and secure deployment of such a security architecture on a distributed separation kernel. In particular, we are modeling essential parts of a smart micro grid with several interacting prosumers, and demonstrate exemplary security/privacy requirements of this smart grid. The security policy architecture of this smart grid is deployed on a secure distributed platform, relying on a combination of separation kernels and deterministic network, as developed in the Distributed MILS project.}, doi = {10.1007/978-3-319-10329-7_2}, keywords = {Smart grid security, Distributed MILS, Separation kernel, Formal verification, Security policy architecture, Configuration compiler, Model-based Systems Engineering, MbSE}, } @techreport{quilbeuf2013, author = {Quilbeuf, Jean and Igna, Georgeta and Bytschkow, Denis and Rue{\ss}, Harald}, title = {Security policies for distributed systems}, journal = {arXiv preprint}, volume = {arXiv:1310.3723}, year = {2013}, month = oct, school = {arXiv preprint}, abstract = {A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run in separation, and possible process communication on a technical platform is restricted to specified message paths of the system. Furthermore, we propose to further restrict the allowable information flow by adding filter functions for controlling which messages may be transmitted between processes, and we prove that locally checking filter functions is sufficient for ensuring global security policies. Altogether, global intransitive security policies are established by means of local verification conditions for the (trusted) processes of the distributed system. Moreover, security policies may be implemented securely on distributed integration platforms which ensure partitioning. We illustrate our results with a smart grid case study, where we use CTL model checking for discharging local verification conditions for each process under consideration.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://arxiv.org/abs/1310.3723}, }