Software Engineer
RSA is a type of cryptographic technique to enable communication between two parties over an unsecure medium. It was inspired by the work of diffie-hellman in cryptography
A public key is shared between the sender and receiver. The original message is encrypted using the public key and transmitted over to the receiver. The receiver can only decrypt the original message, if they have the private key that is not shared over with anybody.
References:
Accountability and trust are difficult to garner for a company without using data collection and processing techniques that respect an individual's privacy. With growing number of applications employing Artificial Intelligence, web and mobile applications are collecting and processing large data streams and hence the importance of data privacy is going on a steep upward path. In the wake of it's growing importance, a new line of research in theoretical computer science emerged to be known as differential privacy. Differential privacy has provided a framework for computing on sensitive datasets in which one can mathematically prove the privacy of individual-specific information.
Definition : M : 𝒳n X 𝒬 → 𝒴 is differentially private iff ∀ q ∈ 𝒬, and ∀ x, x' ∈ 𝒳 differing only on a single row, the distributions M(x, q) and M(x', q) are similar
Here, 𝒳 is the space from which we get rows, 𝒬 is the space of questions, and 𝒴 is the output space. The main idea behind the definition is that no individual's data has a significant influence on the output
In addition to this, private learning is a combination of probably approximate correct learning and differential privacy. Thus, we collect labeled individual information, and output a hypothesis while preserving the privacy of each individual.
Google just announced TensorFlow privacy module - thus enabling machine learning with differential privacy in their TensorFlow framework
References:
Timed automata are a subclass of Hybrid Automata and were introduced by Alur and Dill [1] in 1994 to model real-time systems. They are very useful in formal verification because the problem of reachability analysis on timed automata is a "decidable" problem. In computability theory, a decidable problem is a decision problem that has an algorithm solution that returns either true or false, hence known as decidable. When we are interested in modeling timed systems that have real-time timing constraints this class of automata are incredibly useful. Some examples of timing constraints are - "The airbag has to open within 5ms after a car crashes" or "The pacemaker needs to generate impulses within a real-time constraint of heart beat falling below a certain threshold". A timed automaton is composed of a finite automaton and a set of clocks.
All the clock values increase at a same pace. Guards can be placed on the transitions of the automaton using which we can enable or disable that transition, thereby constraining the behaviour of the automaton and making it dependable on the clock values. Guards are nothing but clock values compared to integers and can either evaluate to true or false. We need to note here that the clocks can be reset.
A timed automaton can be formally defined as a tuple H= (Q, Σ, C, E, q0, F). Here Q is a finite set, the elements of Q are states of automaton A. Σ is a finite set called actions of A. C is a finite set called the clocks of A. E is a set of edges called transitions of A. q0 is an element of Q, called the initial state. An edge defined by (q,a,g,r,q') from E is a transition from state q to q' with action a, guard g and clock resets r [2], F is the set of final states.
Thanks to the references
Predicate-abstraction is a powerful technique for extracting finite-state models from infinite state systems. Let us first look at what predicate abstraction is and how it is helping us in model checking. An abstract state is a valid combination of truth values to the predicates, and hence corresponds to a polyhedral set of the concrete state space. In predicate abstraction, a finite set of predicates is defined over the concrete set of states. These predicates are used to construct a finite state abstration of the concrete system. The finite model can be used in place of the original system when performing model checking or deriving invariants.
An n-dimensional linear hybrid system is a tuple H= (X, L, X0, I, f, T). X is a convex polyhedron representing the hybrid state space. L is a finite set of locations. X0 is a set of initial states. f: L->(Rn->Rn) assigns to each location a continuous vector field f(l) on x. T is a relation capturing discrete transition jumps between two discrete locations.
In hardware domain, one of the most common abstraction techniques is localization reduction. This technique is an over-approximation of original circuit for reachability properties. This means if the abstraction satisfies the property, the property also holds on original circuit. The drawback is that when the model checking of the abstraction fails. It may produce a counterexample that maynot correspond to any concrete counterexample, which is known as a spurious counterexample. Several techniques to overcome this problem have been proposed, which make use of techniques like word level predicate abstraction.
In Progress..When we design a new system, an important question that ususally pops up is - How do we ensure dependability and performance of the system ? With recent advances in ubiquitous computing, systems are getting more complicated. Networking and wireless are becoming a more common phenomena across these devices. Systems are becoming context-aware and adaptive. Many suggest a transformation in the conventional software engineering flows and coming up with model-based software engineering and model-based verification techniques.
To rule out errors, one must consider all possible executions in a program, which is often not possible mechanically. Given that computer systems are getting sophisticated, this has become more difficult to achieve. Formal Verification (FV) domain provides us with effective techniques for the same. There are various techniques ranging from manual mathematical proofs to fast, lightweight static analysis methods. We focus on model-checking, that is fully-automatic and exhaustive in terms of state space coverage.
Automatic Model Checking techniques give assurance of a safe, dependable system with a good performance and trust in security and privacy. However we want to discuss probabilistic model checking. We want to capture probability and resource usage in a computer system. Probability is an effective tool to model uncertainty and performance of a system. By doing so, we quantify the rate of failures and express Quality of Service (QoS). It is used in an evidence based statistical analysis of behaviours to quantify terms like trust and anonymity.
Probabilistic Model Checking is an FV technique for modelling and verifying systems that exhibit stochastic behaviour. Three most commonly used probabilistic models are:
Microservices are an important trend that have emerged in the enterprise often associated with the DevOps culture. These practices are designed to offer greater agility and operational efficiency. These came into being at companies like Amazon, Netflix, SoundCloud, Google, Facebook and several others which build software at scale.
Set this up out of curiosity.