CÁC BÀI BÁO KHOA HỌC 06:27:50 Ngày 18/08/2019 GMT+7
Information flow is linear refinement of constancy

Detecting information flows inside a program is useful to check non-interference of program variables, an important aspect of software security. Information flows have been computed in the past by using abstract interpretation over an abstract domain IF which expresses sets of flows. In this paper we reconstruct IF as the linear refinement C → C of a basic domain C expressing constancy of program variables. This is important since we also show that C → C, and hence IF, is closed w.r.t. linear refinement, and is hence optimal and condensing. Then a compositional, input-independent static analysis over IF has the same precision of a non-compositional, input-driven analysis. Moreover, we show that C → C has a natural representation in terms of Boolean formulas, efficiently implementable through binary decision diagrams. © Springer-Verlag Berlin Heidelberg 2005.


 Spoto F.
   721.pdf    Gửi cho bạn bè
  Từ khóa : Boolean algebra; Computer software; Computer system firewalls; Information technology; Security of data; Information flow; Linear refinement; program variables; software security; Data flow analysis