-
Towards a Transpiler for C/C++ to Safer Rust
Authors:
Dhiren Tripuramallu,
Swapnil Singh,
Shrirang Deshmukh,
Srinivas Pinisetty,
Shinde Arjun Shivaji,
Raja Balusamy,
Ajaganna Bandeppa
Abstract:
Rust is a multi-paradigm programming language developed by Mozilla that focuses on performance and safety. Rust code is arguably known best for its speed and memory safety, a property essential while develo** embedded systems. Thus, it becomes one of the alternatives when develo** operating systems for embedded devices. How to convert an existing C++ code base to Rust is also gaining greater a…
▽ More
Rust is a multi-paradigm programming language developed by Mozilla that focuses on performance and safety. Rust code is arguably known best for its speed and memory safety, a property essential while develo** embedded systems. Thus, it becomes one of the alternatives when develo** operating systems for embedded devices. How to convert an existing C++ code base to Rust is also gaining greater attention. In this work, we focus on the process of transpiling C++ code to a Rust codebase in a robust and safe manner. The manual transpilation process is carried out to understand the different constructs of the Rust language and how they correspond to C++ constructs. Based on the learning from the manual transpilation, a transpilation table is created to aid in future transpilation efforts and to develop an automated transpiler. We also studied the existing automated transpilers and identified the problems and inefficiencies they involved. The results of the transpilation process were closely monitored and evaluated, showing improved memory safety without compromising performance and reliability of the resulting codebase. The study concludes with a comprehensive analysis of the findings, an evaluation of the implications for future research, and recommendations for the same in this area.
△ Less
Submitted 16 January, 2024;
originally announced January 2024.
-
Runtime Monitoring and Statistical Approaches for Correlation Analysis of ECG and PPG
Authors:
Abhinandan Panda,
Srinivas Pinisetty,
Partha Roop
Abstract:
Biophysical signals such as Electrocardiogram (ECG) and Photoplethysmogram (PPG) are key to the sensing of vital parameters for wellbeing. Coincidentally, ECG and PPG are signals, which provide a "different window" into the same phenomena, namely the cardiac cycle. While they are used separately, there are no studies regarding the exact correction of the different ECG and PPG events. Such correlat…
▽ More
Biophysical signals such as Electrocardiogram (ECG) and Photoplethysmogram (PPG) are key to the sensing of vital parameters for wellbeing. Coincidentally, ECG and PPG are signals, which provide a "different window" into the same phenomena, namely the cardiac cycle. While they are used separately, there are no studies regarding the exact correction of the different ECG and PPG events. Such correlation would be helpful in many fronts such as sensor fusion for improved accuracy using cheaper sensors and attack detection and mitigation methods using multiple signals to enhance the robustness, for example. Considering this, we present the first approach in formally establishing the key relationships between ECG and PPG signals. We combine formal run-time monitoring with statistical analysis and regression analysis for our results.
△ Less
Submitted 20 January, 2022;
originally announced February 2022.
-
Runtime Interchange for Adaptive Re-use of Intelligent Cyber-Physical System Controllers
Authors:
Hammond Pearce,
Xin Yang,
Srinivas Pinisetty,
Partha S. Roop
Abstract:
Cyber-Physical Systems (CPSs) such as those found within autonomous vehicles are increasingly adopting Artificial Neural Network (ANN)-based controllers. To ensure the safety of these controllers, there is a spate of recent activity to formally verify the ANN-based designs. There are two challenges with these approaches: (1) The verification of such systems is difficult and time consuming. (2) The…
▽ More
Cyber-Physical Systems (CPSs) such as those found within autonomous vehicles are increasingly adopting Artificial Neural Network (ANN)-based controllers. To ensure the safety of these controllers, there is a spate of recent activity to formally verify the ANN-based designs. There are two challenges with these approaches: (1) The verification of such systems is difficult and time consuming. (2) These verified controllers are not able to adapt to frequent requirements changes, which are typical in situations like autonomous driving. This raises the question: how can trained and verified controllers, which have gone through expensive training and verification processes, be re-used to deal with requirement changes? This paper addresses this challenge for the first time by proposing a new framework that is capable of dealing with requirement changes at runtime through a mechanism we term runtime interchange. Our approach functions via a continual exchange and selection process of multiple pre-verified controllers. It represents a key step on the way to component-oriented engineering for intelligent designs, as it preserves the behaviours of the original controllers while introducing additional functionality. To demonstrate the efficacy of our approach we utilise an existing autonomous driving case study as well as a set of smaller benchmarks. These show that introduced overheads are extremely minimal and that the approach is very scalable.
△ Less
Submitted 23 September, 2021;
originally announced October 2021.
-
Monitoring Data Minimisation
Authors:
Srinivas Pinisetty,
Thibaud Antignac,
David Sands,
Gerardo Schneider
Abstract:
Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking that a program satisfies the data minimisation principle is not easy, even for the simple case when considering deterministic programs-as-functions. In this paper we prove (im)possibility results concerning runtime monito…
▽ More
Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking that a program satisfies the data minimisation principle is not easy, even for the simple case when considering deterministic programs-as-functions. In this paper we prove (im)possibility results concerning runtime monitoring of (non-)minimality for deterministic programs both when the program has one input source (monolithic) and for the more general case when inputs come from independent sources (distributed case). We propose monitoring mechanisms where a monitor observes the inputs and the outputs of a program, to detect violation of data minimisation policies. We show that monitorability of (non) minimality is decidable only for specific cases, and detection of satisfaction of different notions of minimality in undecidable in general. That said, we show that under certain conditions monitorability is decidable and we provide an algorithm and a bound to check such properties in a pre-deployment controlled environment, also being able to compute a minimiser for the given program. Finally, we provide a proof-of-concept implementation for both offline and online monitoring and apply that to some case studies.
△ Less
Submitted 5 January, 2018;
originally announced January 2018.
-
Runtime enforcement of reactive systems using synchronous enforcers
Authors:
Srinivas Pinisetty,
Partha S Roop,
Steven Smyth,
Stavros Tripakis,
Reinhard von Hanxleden
Abstract:
Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of…
▽ More
Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of a synchronous program and (minimally) edits erroneous inputs/outputs in order to guarantee that a given property holds. We define enforceability conditions, develop an online enforcement algorithm, and prove its correctness. We also report on an implementation of the algorithm on top of the KIELER framework for the SCCharts synchronous language. Experimental results show that enforcement has minimal execution time overhead, which decreases proportionally with larger benchmarks.
△ Less
Submitted 15 December, 2016;
originally announced December 2016.
