Oblivious algebraic data types

Secure computation allows multiple parties to compute joint functions over private data without leaking any sensitive data, typically using powerful cryptographic techniques. Writing secure applications using these techniques directly can be challenging, resulting in the development of several programming languages and compilers that aim to make secure computation accessible. Unfortunately, many of these languages either lack or have limited support for rich recursive data structures, like trees. In this paper, we propose a novel representation of structured data types, which we call oblivious algebraic data types, and a language for writing secure computations using them. This language combines dependent types with constructs for oblivious computation, and provides a security-type system which ensures that adversaries can learn nothing more than the result of a computation. Using this language, authors can write a single function over private data, and then easily build an equivalent secure computation according to a desired public view of their data.

Monotone recursive types and recursive data representations in Cedille

Guided by Tarksi’s fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time roll and unroll operations within Cedille, an impredicative, constructive, and logically consistent pure typed lambda calculus. This derivation takes place within the preorder on Cedille types induced by type inclusions, a notion which is expressible within the theory itself. As applications, we use monotone recursive types to generically derive two recursive representations of data in lambda calculus, the Parigot and Scott encoding. For both encodings, we prove induction and examine the computational and extensional properties of their destructor, iterator, and primitive recursor in Cedille. For our Scott encoding in particular, we translate into Cedille a construction due to Lepigre and Raffalli (2019) that equips Scott naturals with primitive recursion, then extend this construction to derive a generic induction principle. This allows us to give efficient and provably unique (up to function extensionality) solutions for the iteration and primitive recursion schemes for Scott-encoded data.

Localization Algorithm for 3D Sensor Networks: A Recursive Data Fusion Approach

Location-based applications for security and assisted living, such as human location tracking, pet tracking and others, have increased considerably in the last few years, enabled by the fast growth of sensor networks. Sensor location information is essential for several network protocols and applications such as routing and energy harvesting, among others. Therefore, there is a need for developing new alternative localization algorithms suitable for rough, changing environments. In this paper, we formulate the Recursive Localization (RL) algorithm, based on the recursive coordinate data fusion using at least three anchor nodes (ANs), combined with a multiplane location estimation, suitable for 3D ad hoc environments. The novelty of the proposed algorithm is the recursive fusion technique to obtain a reliable location estimation of a node by combining noisy information from several nodes. The feasibility of the RL algorithm under several network environments was examined through analytic formulation and simulation processes. The proposed algorithm improved the location accuracy for all the scenarios analyzed. Comparing with other 3D range-based positioning algorithms, we observe that the proposed RL algorithm presents several advantages, such as a smaller number of required ANs and a better position accuracy for the worst cases analyzed. On the other hand, compared to other 3D range-free positioning algorithms, we can see an improvement by around 15.6% in terms of positioning accuracy.

A Multilayer Iteration-Based Improved Recursive Data Flow Matching Algorithm

Differentiated service for packets entering the network is available through packet matching. Network security and differentiated services mean an inevitable choice for routers. Recursive data flow matching algorithm (RFC) is a high performance packet matching algorithm. However, with the increase of rule dimension and scale in the rule base, system memory consumption is unavoidable. This paper lowers memory consumption via improvement on RFC by dividing the rule base into several subsets and storing each rule in a separate subset. In addition, a variety of methods are used to streamline the RFC data structure for further improvement in algorithm speed and memory performance. The experimental results show that the improved algorithm of RFC greatly reduces the overall memory consumption of RFC, while greatly improving package matching performance.

Applying Program Transformations for Deductive Verification of the List Reverse Program

The program transformation methods to simplify the deductive verification of programs with recursive data types are investigated. The list reversion program is considered as an example. A source program in the C language is translated to the cP functional language which includes no pointers. The resulting program is translated further to the WhyML language to perform deductive verification of the program. The cP language includes the same constructs of the C language except pointers. In the C program, all actions that include pointers are replaced by the equivalent fragments without pointers. These replacement are performed by the special transformations using the results of the program dataflow analysis. Three variants of deductive verification of the transformed list reverse program in the Why3 verification platform with SMT solvers (Z3 4.8.6, CVC3 2.4.1, CVC4 1.7) are performed. First, the recursive WhyML program supplied with specifications was automatically verified successfully using only SMT solvers. Second, the recursive program was translated to the P predicate language. Correctness formulae were constructed for the P program and translated further to the why3 specification language. The formulae proving correctness were easy like the first variant. But correctness formulae for the first and second variants were different. Third, the "imperative" WhyML program that included while loop with additional invariant specifications was verified. The proving was easy but not automatic. So, for deductive verification, recursive program variant appears to be more preferable against imperative program variant.

Parsing Character Arrays by Recursive Scoping and Structuring Using the Example of VRML Data

Parsing character arrays by recursive scoping and structuring using the example of VRML data. The article presents a new method for structuring, segmentation and algorithmic design of the parser of character arrays using the example of VRML data. The key feature of the method is the ability to form a hierarchically complex object by means of recursive data structuring, which makes it possible to cover in aggregate the entire contents of the object, including its arbitrary nesting of child objects. This leads to high controllability of the development of the parsing algorithm, allowing you to focus each time on a specific piece of data, while not losing sight of the entire aggregate connectivity of information. The results obtained can easily be used in plans for creating convenient data storage structures related to information security, solving the problem of containing the amount of data in files, managing big data in heterogeneous systems, and processing hierarchical data in the Internet of Things. Keywords: data analysis method, parsing, structuring, se

Syntactic Analysis of Graphical Information Using Recursive Scoping

The report presents a new method for structuring, segmentation, and algorithmic design of the character array parser using VRML data as an example. The key feature of the method is the possibility of forming a hierarchically complex object by means of recursive data structuring, which allows you to cover the entire contents of the object, including its arbitrary nesting of child objects. This leads to a highly manageable development of the parsing algorithm, allowing you to focus each time on a specific piece of data, while not losing sight of the entire aggregate coherence of the information. The results obtained can easily be used in plans for creating convenient data storage structures related to information security, solving the problem of containing the amount of data in files, data management problems in heterogeneous systems, and hierarchical data solutions in the Internet of Things.