Abstract: Information Flow Control (IFC) is a form of dependence analysis that tracks and prohibits dependence of public outputs on secret inputs. Such a dependence analysis is often carried out using a type system. IFC type systems can track dependence (via confidentiality labels) at varying levels of granularity. On one extreme, there are fine-grained type systems that track dependence at the level of individual values. They label individual values. On the other extreme, there are coarse-grained type systems that track dependence at the level of entire computations. These type systems do not label individual values but instead label entire sub-computations. An…important foundational question is one of the relative expressiveness of these two classes of IFC type systems. In this paper we show that, despite the glaring differences in how they track dependence, the two classes of type systems are actually equally expressive. We do this by showing translations from FG, a fine-grained IFC type system derived from SLAM (In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (1998)), to SLIO ∗ , a coarse-grained IFC type system derived from HLIO (In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP) (2015)), and vice-versa. The translation from SLIO ∗ to FG is straightforward since FG tracks dependence at a granularity finer than SLIO ∗ does. However, the translation from FG to SLIO ∗ is quite involved and relies extensively on label quantification. We further examine the reason for this complexity using a slight variant of SLIO ∗ , called CG, to which FG can be translated more easily. As a separate, more foundational contribution we show how to extend logical relation models of information flow to languages with higher-order state. Specifically, we build world-indexed (Kripke) logical relations for FG, SLIO ∗ and CG, which we use to prove these type systems sound and also to prove the translations between them correct.
Show more
Keywords: Information flow control, type systems, typed translation, logical relations, type system expressiveness
Abstract: We present the design, proof theory and metatheory of a logic for representing and reasoning about authorization policies. A salient feature of the logic, BL, is its support for system state in the form of interpreted predicates, upon which authorization policies often rely. In addition, BL includes Abadi et al.'s “says” connective and explicit time. BL is illustrated through a case study of policies for sharing sensitive information created in the US intelligence community. We discuss design choices in the interaction between state and other features of BL and validate BL's proof theory by proving standard metatheoretic properties like admissibility…of cut.
Show more
Abstract: Sequential pattern mining is a vital problem with broad applications. However, it is also challenging, as combinatorial high number of intermediate subsequences are generated that have to be critically examined. Most of the basic solutions are based on the assumption that the mining is performed on static database. But modern day databases are being continuously updated and are dynamic in nature. So, incremental mining of sequential patterns has become the norm. This article investigates the need for incremental mining of sequential patterns. An analytical study, focusing on the characteristics, has been made for more than twenty incremental mining algorithms. Further,…we have discussed the issues associated with each of them. We infer that the better approach is incremental mining on the progressive database. The three more relevant algorithms, based on this approach, are also studied in depth along with the other work done in this area. This would give scope for future research direction.
Show more
Abstract: Information flow control (IFC) has been extensively studied as an approach to mitigate information leaks in applications. A vast majority of existing work in this area is based on static analysis. However, some applications, especially on the Web, are developed using dynamic languages like JavaScript where static analyses for IFC do not scale well. As a result, there has been a growing interest in recent years to develop dynamic or runtime information flow analysis techniques. In spite of the advances in the field, runtime information flow analysis has not been at the helm of information flow security, one of the reasons…being that the analysis techniques and the security property related to them (non-interference) over-approximate information flows (particularly implicit flows), generating many false positives. In this paper, we present a sound and precise approach for handling implicit leaks at runtime. In particular, we present an improvement and enhancement of the so-called permissive-upgrade strategy, which is widely used to tackle implicit leaks in dynamic information flow control. We improve the strategy’s permissiveness and generalize it. Building on top of it, we present an approach to handle implicit leaks when dealing with complex features like unstructured control flow and exceptions in higher-order languages. We explain how we address the challenge of handling unstructured control flow using immediate post-dominator analysis. We prove that our approach is sound and precise.
Show more