Integrating Information Flow Analysis in Unifying Theories of Programming

Chunyan Mu; Guoqiang Li

doi:10.1109/PRDC53464.2021.00018

Integrating Information Flow Analysis in Unifying Theories of Programming

Chunyan Mu, Guoqiang Li

Shanghai Jiao Tong University

Research output: Chapter in Book/Report/Conference proceeding › Published conference contribution

1 Downloads (Pure)

Abstract

This paper presents a formal approach for modelling and reasoning about information flow control in software systems under Hoare and He's Unifying Theories of Programming (UTP). We investigate the problem of integrating information flow control into system design in a unified semantic setting. Our approach can therefore treat information flow analysis and control in various families of specification languages and programming paradigms in a more general way. In addition, we formalise the link between classes of predicates as a paired function which maps set of the predicates from one class into set of the predicates from the other with a concern of flow security preservation. The proposed flow-sensitive combined theories of multiple level classes of predicates can be applied to ensure flow security in different paradigms under stepwise development.

Original language	English
Title of host publication	2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing
Publisher	IEEE Computer Society
Pages	67-76
Number of pages	10
ISBN (Electronic)	9781665424769
ISBN (Print)	9781665424776
DOIs	https://doi.org/10.1109/PRDC53464.2021.00018
Publication status	Published - 12 Jan 2022
Event	IEEE 26th Pacific Rim International Symposium on Dependable Computing - Perth, Australia Duration: 1 Dec 2021 → 4 Dec 2021

Publication series

Name	Proceedings (IEEE Pacific Rim International Symposium on Dependable Computing)
Publisher	IEEE
ISSN (Print)	1555-094X
ISSN (Electronic)	2473-3105

Conference

Conference	IEEE 26th Pacific Rim International Symposium on Dependable Computing
Abbreviated title	PRDC
Country/Territory	Australia
City	Perth
Period	1/12/21 → 4/12/21

Bibliographical note

This research is supported by the China National R&D Key Research Program (2019YFB1705703) and the In-terdisciplinary Program of SJTU, Shanghai, China (No. YG2019ZDA07).

Access to Document

10.1109/PRDC53464.2021.00018Licence: Unspecified

Mu_etLi_PRDC_Imtegrating_Information_Flow
© 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. The final published version is available at: C. Mu and G. Li, "Integrating Information Flow Analysis in Unifying Theories of Programming," 2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing (PRDC), Perth, Australia, 2021, pp. 67-76, doi: 10.1109/PRDC53464.2021.00018.
Accepted author manuscript, 206 KBLicence: Other

Cite this

Integrating Information Flow Analysis in Unifying Theories of Programming. / Mu, Chunyan; Li, Guoqiang.
2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing. IEEE Computer Society, 2022. p. 67-76 ( Proceedings (IEEE Pacific Rim International Symposium on Dependable Computing)).

Research output: Chapter in Book/Report/Conference proceeding › Published conference contribution

Mu, C & Li, G 2022, Integrating Information Flow Analysis in Unifying Theories of Programming. in 2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing. Proceedings (IEEE Pacific Rim International Symposium on Dependable Computing), IEEE Computer Society, pp. 67-76, IEEE 26th Pacific Rim International Symposium on Dependable Computing, Perth, Australia, 1/12/21. https://doi.org/10.1109/PRDC53464.2021.00018

@inproceedings{b05f28185c6647feb25919a8c7191c09,

title = "Integrating Information Flow Analysis in Unifying Theories of Programming",

abstract = "This paper presents a formal approach for modelling and reasoning about information flow control in software systems under Hoare and He's Unifying Theories of Programming (UTP). We investigate the problem of integrating information flow control into system design in a unified semantic setting. Our approach can therefore treat information flow analysis and control in various families of specification languages and programming paradigms in a more general way. In addition, we formalise the link between classes of predicates as a paired function which maps set of the predicates from one class into set of the predicates from the other with a concern of flow security preservation. The proposed flow-sensitive combined theories of multiple level classes of predicates can be applied to ensure flow security in different paradigms under stepwise development.",

author = "Chunyan Mu and Guoqiang Li",

note = "This research is supported by the China National R&D Key Research Program (2019YFB1705703) and the In-terdisciplinary Program of SJTU, Shanghai, China (No. YG2019ZDA07).; IEEE 26th Pacific Rim International Symposium on Dependable Computing, PRDC ; Conference date: 01-12-2021 Through 04-12-2021",

year = "2022",

month = jan,

day = "12",

doi = "10.1109/PRDC53464.2021.00018",

language = "English",

isbn = "9781665424776",

series = " Proceedings (IEEE Pacific Rim International Symposium on Dependable Computing)",

publisher = "IEEE Computer Society",

pages = "67--76",

booktitle = "2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing",

}

TY - GEN

T1 - Integrating Information Flow Analysis in Unifying Theories of Programming

AU - Mu, Chunyan

AU - Li, Guoqiang

N1 - This research is supported by the China National R&D Key Research Program (2019YFB1705703) and the In-terdisciplinary Program of SJTU, Shanghai, China (No. YG2019ZDA07).

PY - 2022/1/12

Y1 - 2022/1/12

N2 - This paper presents a formal approach for modelling and reasoning about information flow control in software systems under Hoare and He's Unifying Theories of Programming (UTP). We investigate the problem of integrating information flow control into system design in a unified semantic setting. Our approach can therefore treat information flow analysis and control in various families of specification languages and programming paradigms in a more general way. In addition, we formalise the link between classes of predicates as a paired function which maps set of the predicates from one class into set of the predicates from the other with a concern of flow security preservation. The proposed flow-sensitive combined theories of multiple level classes of predicates can be applied to ensure flow security in different paradigms under stepwise development.

AB - This paper presents a formal approach for modelling and reasoning about information flow control in software systems under Hoare and He's Unifying Theories of Programming (UTP). We investigate the problem of integrating information flow control into system design in a unified semantic setting. Our approach can therefore treat information flow analysis and control in various families of specification languages and programming paradigms in a more general way. In addition, we formalise the link between classes of predicates as a paired function which maps set of the predicates from one class into set of the predicates from the other with a concern of flow security preservation. The proposed flow-sensitive combined theories of multiple level classes of predicates can be applied to ensure flow security in different paradigms under stepwise development.

U2 - 10.1109/PRDC53464.2021.00018

DO - 10.1109/PRDC53464.2021.00018

M3 - Published conference contribution

SN - 9781665424776

T3 - Proceedings (IEEE Pacific Rim International Symposium on Dependable Computing)

SP - 67

EP - 76

BT - 2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing

PB - IEEE Computer Society

T2 - IEEE 26th Pacific Rim International Symposium on Dependable Computing

Y2 - 1 December 2021 through 4 December 2021

ER -

Integrating Information Flow Analysis in Unifying Theories of Programming

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this