The teaching and development of the necessary skills to efficiently implement and develop Internet of Things (IoT) sensor devices is particularly challenging. Traditionally, the development of these ...skills is achieved with the help of several laboratorial facilities. Here, a full‐stack model to help in this process is presented. This model includes the utilization of a set of tools that can be used to remotely access the available resources, thus creating an “online lab.” This “online lab” is of particular interest and usefulness in the current pandemic context and is of particular interest not only for students to have access to real hardware devices, thus developing their skills and knowledge, but also to professional teams collaborating in the development of IoT sensor devices.
Verified low-level programming embedded in F Protzenko, Jonathan; Zinzindohoué, Jean-Karim; Rastogi, Aseem ...
Proceedings of ACM on programming languages,
09/2017, Letnik:
1, Številka:
ICFP
Journal Article
Recenzirano
Odprti dostop
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, ...well-behaved subset of C in F*, a dependently- typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code.
By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.
We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.
A set of works aimed at optimizing certain administrative processes of Windows operating systems is done. A classification of administration tasks has been developed in order to determine both ...labor-intensive and routine administration tasks, as well as tasks requiring and allowing automation. Based on preselected criteria a comparative analysis of administration tools, including built-in and open source utilities is made. A plugin for the Process Hacker utility, which allows creating and control of the list of allowed and conditionally prohibited programs in Windows 7 SP1, Windows 8, Windows 10 operating systems has been developed and deployed.
Optimal coordination of directional overcurrent relays (DOCRs) in interconnected power systems is a highly constrained, non-convex and non-linear optimisation problem. In this study, use of a series ...of linear programming (LP) problems in a variable neighbourhood search (VNS) framework is proposed, in which pickup current settings can be considered either as continuous or discrete variables. Therefore, the proposed hybrid algorithm (VNS–LP) is suitable for coordination problem-solving in a network with different types of DOCRs. Furthermore, two versions of the VNS algorithm are proposed, the first of which is very easy to implement, while, the other is somewhat more sophisticated, and at the same time much faster and possibly suitable for online coordination in smart grids applications. One advantage of the second algorithm is that it relies only on elementary arithmetic and requires low RAM, which makes it implementable in any low-level programming environment. This, in turn, can increase the interoperability, which is of crucial importance when automating tasks. The efficiency of the proposed algorithm was investigated in several test systems. Numerical results indicate that the two proposed approaches outperform the previous methods. Moreover, the coordination problem is solved in a reasonably short time using a faster approach.
The main goal of the artifact is to support the experimental claims of the paper #992 "Interface Compliance of Inline As-sembly: Automatically Check, Patch and Refine" by making both the prototype ...and data availableto the community. The expected result is the same output as the figures given in Table I and Table IV (appendix C) of the paper. In addition, we hope the released snapshot of our prototype is simple, documented and robust enough to have some uses for people dealing withinline assembly.
Interface Compliance of Inline Assembly Recoules, Frédéric; Bardin, Sébastien; Bonichon, Richard ...
2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE),
05/2021
Conference Proceeding
Odprti dostop
Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes in the GNU syntax ...(supported by major compilers such as GCC, Clang and ICC) have an interface specifying how the assembly codes interact with the C environment. For simplicity reasons, the compiler treats GNU inline assembly codes as blackboxes and relies only on their interface to correctly glue them into the compiled C code. Therefore, the adequacy between the assembly chunk and its interface (named compliance) is of primary importance, as such compliance issues can lead to subtle and hard-to-find bugs. We propose RUSTInA, the first automated technique for formally checking inline assembly compliance, with the extra ability to propose (proven) patches and (optimization) refinements in certain cases. RUSTInA is based on an original formalization of the inline assembly compliance problem together with novel dedicated algorithms. Our prototype has been evaluated on 202 Debian packages with inline assembly (2656 chunks), finding 2183 issues in 85 packages - 986 significant issues in 54 packages (including major projects such as ffmpeg or ALSA), and proposing patches for 92% of them. Currently, 38 patches have already been accepted (solving 156 significant issues), with positive feedback from development teams.
Rigel Kelm, John H.; Johnson, Daniel R.; Johnson, Matthew R. ...
Proceedings of the 36th annual international symposium on Computer architecture,
06/2009
Conference Proceeding
This paper considers Rigel, a programmable accelerator architecture for a broad class of data- and task-parallel computation. Rigel comprises 1000+ hierarchically-organized cores that use a ...fine-grained, dynamically scheduled single-program, multiple-data (SPMD) execution model. Rigel's low-level programming interface adopts a single global address space model where parallel work is expressed in a task-centric, bulk-synchronized manner using minimal hardware support. Compared to existing accelerators, which contain domain-specific hardware, specialized memories, and/or restrictive programming models, Rigel is more flexible and provides a straightforward target for a broader set of applications.
We perform a design analysis of Rigel to quantify the compute density and power efficiency of our initial design. We find that Rigel can achieve a density of over 8 single-precision GFLOPS/mm2 in 45nm, which is comparable to high-end GPUs scaled to 45nm. We perform experimental analysis on several applications ported to the Rigel low-level programming interface. We examine scalability issues related to work distribution, synchronization, and load-balancing for 1000-core accelerators using software techniques and minimal specialized hardware support. We find that while it is important to support fast task distribution and barrier operations, these operations can be implemented without specialized hardware using flexible hardware primitives.
Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control-flow graphs, which are not available when dealing with ...self-modifying programs which can modify their own code at runtime. We formalize in the Coq proof assistant some key abstract interpretation techniques that automatically extract memory safety properties from binary code. Our analyzer is formally proved correct and has been run on several self-modifying challenges, provided by Cai et al. in their PLDI 2007 article.
Recently web service composition has become a very cost-effective way to develop business applications. However, owing to the unreliable nature of web services, providing the transactional support in ...execution of a service composition is an important design requirement. To guarantee the transactional execution of service compositions, a fault-handling routine has to be started once a service failure occurs in order to undo the effect of previously completed services by calling their corresponding compensation operations. Currently this fault-handling mechanism is implemented by means of low-level programming constructs such as exception-handling mechanism in languages such as WS-BPEL. However, since the logic of handling service failures might become very complex in some applications, this concern should be separated from the normal flow of the composition workflow based on the separation of concerns principle. To achieve this, in this study we have proposed an orchestration pattern for building a transactional service composition in which the failure-recovery logic is imposed on the composition workflow by a Labelled Transition System (LTS) as a separate module. It is assumed that each service within the composition is associated with two known transactional properties: (i) a rollback cost that indicates the cost of undoing (compensating) the service and (ii) a failure probability. The transactional logic of the service composition is also specified using the rollback dependencies represented in a rollback graph. An LTS then is generated to schedule the execution of services within the composition based on the composition transactional logic and properties such that upon a service failure, a recovery path with the lowest cost is followed.
PDF
