-
Pifthon: A Compile-Time Information Flow Analyzer For An Imperative Language
Authors:
Sandip Ghosal,
R. K. Shyamasundar
Abstract:
Compile-time information flow analysis has been a promising technique for protecting confidentiality and integrity of private data. In the last couple of decades, a large number of information flow security tools in the form of run-time execution-monitors or static type systems have been developed for programming languages to analyze information flow security policies. However, existing flow analy…
▽ More
Compile-time information flow analysis has been a promising technique for protecting confidentiality and integrity of private data. In the last couple of decades, a large number of information flow security tools in the form of run-time execution-monitors or static type systems have been developed for programming languages to analyze information flow security policies. However, existing flow analysis tools lack in precision and usability, which is the primary reason behind not being widely adopted in real application development. In this paper, we propose a compile-time information flow analysis for an imperative program based on a hybrid (mutable + immutable) labelling approach that enables a user to detect information flow-policy breaches and modify the program to overcome violations. We have developed an information flow security analyzer for a dialect of Python language, PyX, called Pifthon using the said approach. The flow-analyzer aids in identifying possible misuse of the information in sequential PyX programs corresponding to a given information flow policy (IFP). Pifthon has distinct advantages like reduced labelling overhead that ameliorates usability, covers a wide range of PyX programs that include termination-and progress-sensitive channels, in contrast to other approaches in the literature. The proposed flow analysis is proved to be sound under the classical non-interference property. Further, case study and experience in the usage of Pifthon are provided.
△ Less
Submitted 10 March, 2021;
originally announced March 2021.
-
An Axiomatic Approach to Detect Information Leaks in Concurrent Programs
Authors:
Sandip Ghosal,
R. K. Shyamasundar
Abstract:
Realizing flow security in a concurrent environment is extremely challenging, primarily due to non-deterministic nature of execution. The difficulty is further exacerbated from a security angle if sequential threads disclose control locations through publicly observable statements like print, sleep, delay, etc. Such observations lead to internal and external timing attacks. Inspired by previous wo…
▽ More
Realizing flow security in a concurrent environment is extremely challenging, primarily due to non-deterministic nature of execution. The difficulty is further exacerbated from a security angle if sequential threads disclose control locations through publicly observable statements like print, sleep, delay, etc. Such observations lead to internal and external timing attacks. Inspired by previous works that use classical Hoare style proof systems for establishing correctness of distributed (real-time) programs, in this paper, we describe a method for finding information leaks in concurrent programs through the introduction of leaky assertions at observable program points. Specifying leaky assertions akin to classic assertions, we demonstrate how information leaks can be detected in a concurrent context. To our knowledge, this is the first such work that enables integration of different notions of non-interference used in functional and security context. While the approach is sound and relatively complete in the classic sense, it enables the use of algorithmic techniques that enable programmers to come up with leaky assertions that enable checking for information leaks in sensitive applications.
△ Less
Submitted 2 March, 2021;
originally announced March 2021.
-
Crowdsensing and privacy in smart city applications
Authors:
Raj Gaire,
Ratan K. Ghosh,
Jongkil Kim,
Alexander Krumpholz,
Rajiv Ranjan,
R. K. Shyamasundar,
Surya Nepal
Abstract:
Smartness in smart cities is achieved by sensing phenomena of interest and using them to make smart decisions. Since the decision makers may not own all the necessary sensing infrastructures, crowdsourced sensing, can help collect important information of the city in near real-time. However, involving people brings of the risk of exposing their private information.This chapter explores crowdsensin…
▽ More
Smartness in smart cities is achieved by sensing phenomena of interest and using them to make smart decisions. Since the decision makers may not own all the necessary sensing infrastructures, crowdsourced sensing, can help collect important information of the city in near real-time. However, involving people brings of the risk of exposing their private information.This chapter explores crowdsensing in smart city applications and its privacy implications.
△ Less
Submitted 19 June, 2018;
originally announced June 2018.
-
Internet of Things (IoT) and Cloud Computing Enabled Disaster Management
Authors:
Raj Gaire,
Chigulapalli Sriharsha,
Deepak Puthal,
Hendra Wijaya,
Jongkil Kim,
Prateeksha Keshari,
Rajiv Ranjan,
Rajkumar Buyya,
Ratan K. Ghosh,
R. K. Shyamasundar,
Surya Nepal
Abstract:
Disaster management demands a near real-time information dissemina-tion so that the emergency services can be provided to the right people at the right time. Recent advances in information and communication technologies enable collection of real-time information from various sources. For example, sensors deployed in the fields collect data about the environment. Similarly, social networks like Twi…
▽ More
Disaster management demands a near real-time information dissemina-tion so that the emergency services can be provided to the right people at the right time. Recent advances in information and communication technologies enable collection of real-time information from various sources. For example, sensors deployed in the fields collect data about the environment. Similarly, social networks like Twitter and Facebook can help to collect data from people in the disaster zone. On one hand, inadequate situation awareness in disasters has been identified as one of the primary factors in human errors with grave consequences such as loss of lives and destruction of critical infrastructure. On the other hand, the growing ubiquity of social media and mobile devices, and pervasive nature of the Internet-of-Things means that there are more sources of outbound traffic, which ultimately results in the creation of a data deluge, beginning shortly after the onset of disaster events, leading to the problem of information tsunami. In addition, security and privacy has crucial role to overcome the misuse of the system for either intrusions into data or overcome the misuse of the information that was meant for a specified purpose. .... In this chapter, we provide such a situation aware application to support disaster management data lifecycle, i.e. from data ingestion and processing to alert dissemination. We utilize cloud computing, Internet of Things and social computing technologies to achieve a scalable, effi-cient, and usable situation-aware application called Cloud4BigData.
△ Less
Submitted 19 June, 2018;
originally announced June 2018.
-
Opacity Proof for CaPR+ Algorithm
Authors:
Anshu S Anand,
R K Shyamasundar,
Sathya Peri
Abstract:
In this paper, we describe an enhanced Automatic Check- pointing and Partial Rollback algorithm(CaP R + ) to realize Software Transactional Memory(STM) that is based on con- tinuous conflict detection, lazy versioning with automatic checkpointing, and partial rollback. Further, we provide a proof of correctness of CaP R+ algorithm, in particular, Opacity, a STM correctness criterion, that precisel…
▽ More
In this paper, we describe an enhanced Automatic Check- pointing and Partial Rollback algorithm(CaP R + ) to realize Software Transactional Memory(STM) that is based on con- tinuous conflict detection, lazy versioning with automatic checkpointing, and partial rollback. Further, we provide a proof of correctness of CaP R+ algorithm, in particular, Opacity, a STM correctness criterion, that precisely captures the intuitive correctness guarantees required of transactional memories. The algorithm provides a natural way to realize a hybrid system of pure aborts and partial rollbacks. We have also implemented the algorithm, and shown its effectiveness with reference to the Red-black tree micro-benchmark and STAMP benchmarks. The results obtained demonstrate the effectiveness of the Partial Rollback mechanism over pure abort mechanisms, particularly in applications consisting of large transaction lengths.
△ Less
Submitted 23 October, 2015;
originally announced October 2015.
-
Approximate Computation of Reach Sets in Hybrid Systems
Authors:
D. Ravi,
R. K. Shyamasundar
Abstract:
One of the most important problems in hybrid systems is the {\em reachability problem}. The reachability problem has been shown to be undecidable even for a subclass of {\em linear} hybrid systems. In view of this, the main focus in the area of hybrid systems has been to find {\em effective} semi-decision procedures for this problem. Such an algorithmic approach involves finding methods of compu…
▽ More
One of the most important problems in hybrid systems is the {\em reachability problem}. The reachability problem has been shown to be undecidable even for a subclass of {\em linear} hybrid systems. In view of this, the main focus in the area of hybrid systems has been to find {\em effective} semi-decision procedures for this problem. Such an algorithmic approach involves finding methods of computation and representation of reach sets of the continuous variables within a discrete state of a hybrid system. In this paper, after presenting a brief introduction to hybrid systems and reachability problem, we propose a computational method for obtaining the reach sets of continuous variables in a hybrid system. In addition to this, we also describe a new algorithm to over-approximate with polyhedra the reach sets of the continuous variables with linear dynamics and polyhedral initial set. We illustrate these algorithms with typical interesting examples.
△ Less
Submitted 7 February, 2002;
originally announced February 2002.
