Large flexible software systems tend to incur “bloat”, here defined as the runtime overhead induced by the accumulation of excess functionality and objects. Removing bloat is hard as these overheads are a side-effect of the same trends that have fuelled software growth. Even defining and measuring bloat is non-trivial, as software doesn’t come with built-in labels that indicate which portions of computation are necessary for a given application and which lead to bloat. Much progress has been made in novel analysis tools that aid (human experts in) the process of finding bloat by highlighting signs of excessive activity and data flow. However, there has been very little research focus on understanding the connection between sources of bloat and its system level implications. In particular, excess resource usage due to bloat could be a significant source of power-performance inefficiencies, but the relation between bloat and energy efficient design remains unexplored. In order to systematically devise effective mechanisms for reaping power-performance benefits through bloat mitigation, we require a deeper insight into exactly when excess features can originate bloat, when the resource overheads of bloat are most pronounced and when bloat matters for power performance. This dissertation explores the problem of software bloat and its energy efficiency implications from multiple perspectives to develop a better understanding of these connections. First, we establish the need for a whole systems perspective in assessing potential energy efficiency benefits of bloat reduction, based on a systematic empirical and analytical study that highlights a curious interplay between bloat, energy proportionality and system bottlenecks. Second, we present a novel static analysis algorithm to perform an automated code transformation for object reuse that mitigates bloat involving the generation of excess temporary objects within loops. Third, we introduce the idea of concern augmented program analysis (CAPA), to identify sources of bloat due to excess features; the technique uses externally supplied information about program concerns and their properties as an abstraction of underlying intent. Fourth, as an early diagnostic aid, we use a statistical topic model to automatically discover latent concerns from source code statements and then correlate these latent concerns with resource usage properties that vary at statement granularity. The statistical model has a built-in sensitivity to the context of individual statements so that it can discover even diffused concerns without any apriori concern information. Together, our findings show that presence of excess features, in itself, may not lead to (runtime) bloat, unless these features have some structural interaction with essential features. Further, the overheads due to such structural interactions, in turn, may not cause substantial bloat in the resource consumption of a long running (server) application unless incurred repeatedly during program execution. Finally, even such bloated resource usage has a pronounced impact on power-performance only if it affects a system bottleneck or a hardware resource that has a high degree of energy proportionality and consumes a high fraction of power compared to the other system resources. We conclude that energy wastage due to bloat need not be an inevitable consequence of over-provisioning flexibility. Instead, the extent to which excess features result in runtime bloat and poor power-performance is determined by certain characteristics of the program structure and of the underlying hardware system --these represent potential control points that could be exercised to develop principled design approaches for mitigating bloat without sacrificing flexibility or productivity.

De nos jours, les ordinateurs sont omniprésents. Tous ces ordinateurs stockent et manipulent de l'information, parfois sensible, d'où l'intérêt de protéger et de confiner la dissémination de cette information. Les mécanismes de contrôle de flux d'information permettent justement d'analyser des programmes manipulant de l'information sensible, afin de prévenir les fuites d'information. Les contributions de cette thèse incluent des techniques d'analyse de programmes pour le contrôle de flux d'information tant qualitatif que quantitatif. Les techniques d'analyse qualitatives permettent la détection et la prévention des fuites d'information. Les techniques quantitatives permettent d'estimer ces fuites afin de décider si elles sont négligeables. / Computers have become widespread nowadays. All these computers store and process information. Often, some of this information is sensitive; hence the need to confine and control its dissemination. An important field in computer science, that is concerned about analysing programs in order to confine and control the release of sensitive information, is the information flow control field. The contributions of this thesis include program analysis techniques for qualitative and quantitative information flow control. Qualitative techniques aim at detecting and preventing information leaks. Quantitative techniques go beyong the detection of information leaks, by estimating the leakage in order to decide whether it is negligeable.

Differentielles Testen ist ein wichtiger Bestandteil der Qualitätssicherung von Software, mit dem Ziel Testeingaben zu generieren, die Unterschiede im Verhalten der Software deutlich machen. Solche Unterschiede können zwischen zwei Ausführungspfaden (1) in unterschiedlichen Programmversionen, aber auch (2) im selben Programm auftreten. In dem ersten Fall werden unterschiedliche Programmversionen mit der gleichen Eingabe untersucht, während bei dem zweiten Fall das gleiche Programm mit unterschiedlichen Eingaben analysiert wird. Die Regressionsanalyse, die Side-Channel Analyse, das Maximieren der Ausführungskosten eines Programms und die Robustheitsanalyse von Neuralen Netzwerken sind typische Beispiele für differentielle Softwareanalysen. Eine besondere Herausforderung liegt in der effizienten Analyse von mehreren Programmpfaden (auch über mehrere Programmvarianten hinweg). Die existierenden Ansätze sind dabei meist nicht (spezifisch) dafür konstruiert, unterschiedliches Verhalten präzise hervorzurufen oder sind auf einen Teil des Suchraums limitiert. Diese Arbeit führt das Konzept des hybriden differentiellen Software Testens (HyDiff) ein: eine hybride Analysetechnik für die Generierung von Eingaben zur Erkennung von semantischen Unterschieden in Software. HyDiff besteht aus zwei parallel laufenden Komponenten: (1) einem such-basierten Ansatz, der effizient Eingaben generiert und (2) einer systematischen Analyse, die auch komplexes Programmverhalten erreichen kann. Die such-basierte Komponente verwendet Fuzzing geleitet durch differentielle Heuristiken. Die systematische Analyse basiert auf Dynamic Symbolic Execution, das konkrete Eingaben bei der Analyse integrieren kann. HyDiff wird anhand mehrerer Experimente evaluiert, die in spezifischen Anwendungen im Bereich des differentiellen Testens ausgeführt werden. Die Resultate zeigen eine effektive Generierung von Testeingaben durch HyDiff, wobei es sich signifikant besser als die einzelnen Komponenten verhält. / Differential software testing is important for software quality assurance as it aims to automatically generate test inputs that reveal behavioral differences in software. The concrete analysis procedure depends on the targeted result: differential testing can reveal divergences between two execution paths (1) of different program versions or (2) within the same program. The first analysis type would execute different program versions with the same input, while the second type would execute the same program with different inputs. Therefore, detecting regression bugs in software evolution, analyzing side-channels in programs, maximizing the execution cost of a program over multiple executions, and evaluating the robustness of neural networks are instances of differential software analysis with the goal to generate diverging executions of program paths. The key challenge of differential software testing is to simultaneously reason about multiple program paths, often across program variants, in an efficient way. Existing work in differential testing is often not (specifically) directed to reveal a different behavior or is limited to a subset of the search space. This PhD thesis proposes the concept of Hybrid Differential Software Testing (HyDiff) as a hybrid analysis technique to generate difference revealing inputs. HyDiff consists of two components that operate in a parallel setup: (1) a search-based technique that inexpensively generates inputs and (2) a systematic exploration technique to also exercise deeper program behaviors. HyDiff’s search-based component uses differential fuzzing directed by differential heuristics. HyDiff’s systematic exploration component is based on differential dynamic symbolic execution that allows to incorporate concrete inputs in its analysis. HyDiff is evaluated experimentally with applications specific for differential testing. The results show that HyDiff is effective in all considered categories and outperforms its components in isolation.

Diploma Thespis is focused on development, parameters and construction of one-phase induction motor underplayed by calculations. Emphasis was dealt to simplify motor development process by developed computer program. Program calculations were approved by parallel by hand calculations and by experimental measuring of real processed motor.

The aim of the thesis is to create a business plan dealing with the expansion of the present enterprise, which will be used when applying for a grant from the European Union. The business plan results from the inner analysis of the company as well as from the analysis of the market. The theoretical part of the thesis introduces crucial solutions and findings which are later applied in the practical part of the thesis. The conclusion includes a brief summary of the whole project as well as future prospects of the company.

The complexity associated with development of networked video games creates a need for tools for verifying a consistent player experience. Some networked games achieve consistency through the lockstep protocol, which requires identical execution of sent commands for players to stay synchronised. In this project a method for testing networked multiplayer lockstep games for synchronisation problems related to nondeterministic behaviour is formulated and evaluated. An integrated fuzzing AI is constructed which tries to cause desynchronisation in the tested game and generate data for analysis using log files. Scripts are used for performing semi-automated test runs and parsing the data. The results show that the test system has potential for finding synchronisation problems if the fuzzing AI is used in conjunction with the regular AI in the tested game, but not for finding the origins of said problems. / Komplexiteten förenad med utveckling av nätverksuppkopplade dataspel skapar ett behov av verktyg för att verifiera en konsistent spelarupplevelse. Vissa nätverksspel hålls konsistenta med hjälp av lockstep-protokollet, vilket kräver identisk exekvering av skickade kommandon för att spelarna ska hållas synkroniserade. I detta projekt formuleras och evalueras en metod för att testa om nätverksuppkopplade flerspelarspel lider av synkroniseringsproblem relaterade till ickedeterministiskt beteende. En integrerad fuzzing-AI konstrueras som försöka orsaka desynkronisering i det testade spelet och generera data för analys med hjälp av loggfiler. Skript används för att utföra halvautomatiserade testkörningar och tolka data. Resultaten visar att testsystemet har potential för att hitta synkroniseringsproblem om fuzzing-AI:n används tillsammans med den vanliga AI:n i det testade spelet, men inte för att hitta de bakomliggande orsakerna till dessa problem.

<p>Bluetooth is the de facto standard for short-range wireless communications. Besides Bluetooth Classic (BC), Bluetooth also consists of Bluetooth Low Energy (BLE) and Bluetooth Mesh (Mesh), two relatively new protocols, paving the way for its domination in the era of IoT and 5G. Meanwhile, attacks against Bluetooth, such as BlueBorne, BleedingBit, KNOB, BIAS, and BThack, have been booming in the past few years, impacting the security and privacy of billions of devices. These attacks exploit both design issues in the Bluetooth specification and vulnerabilities of its implementations, allowing for privilege escalation, remote code execution, breaking cryptography, spoofing, device tracking, etc.</p> <p><br></p> <p>To secure Bluetooth, researchers have proposed different approaches for both Bluetooth specification (e.g., formal analysis) and implementation (e.g., fuzzing). However, existing analyses of the Bluetooth specification and implementations are either done manually, or the automatic approaches only cover a small part of the targets. As a consequence, current research is far from complete in securing Bluetooth.</p> <p><br></p> <p>Therefore, in this dissertation, we propose the following research to provide missing pieces in prior research toward completing Bluetooth security research in terms of both Bluetooth specification and implementations. (i) For Bluetooth security at the specification level, we start from one protocol in Bluetooth, BLE, and focus on the previously unexplored reconnection procedure of two paired BLE devices. We conduct a formal analysis of this procedure defined in the BLE specification to provide security guarantees and identify new vulnerabilities that allow spoofing attacks. (ii) Besides BLE, we then formally verify other security-critical protocols in all Bluetooth protocols (BC, BLE, and Mesh). We provide a comprehensive formal analysis by covering the aspects that prior research fails to include (i.e., all possible combinations of protocols and protocol configurations) and considering a more realistic attacker model (i.e., semi-compromised device). With this model, we are able to rediscover five known vulnerabilities and reveal two new issues that affect BC/BLE dual-stack devices and Mesh devices, respectively. (iii) In addition to the formal analysis of specification security, we propose and build a comprehensive formal model to analyze Bluetooth privacy (i.e., device untraceability) at the specification level. In this model, we convert device untraceability into a reachability problem so that it can be verified using existing tools without introducing false results. We discover four new issues allowed in the specification that can lead to eight device tracking attacks. We also evaluate these attacks on 13 Bluetooth implementations and find that all of them are affected by at least two issues. (iv) At the implementation level, we improve Bluetooth security by debloating (i.e., removing code) Bluetooth stack implementations, which differs from prior automatic approaches, such as fuzzing. We keep only the code of needed functionality by a user and minimize their Bluetooth attack surface by removing unneeded Bluetooth features in both the host stack code and the firmware. Through debloating, we can remove 20 known CVEs and prevent a wide range of attacks again Bluetooth. With the research presented in this thesis, we improve Bluetooth security and privacy at both the specification and implementation levels.</p>

Enforcing security policies to distributed systems is difficult, in particular, when a system contains untrusted components. We designed AspectKE*, a distributed AOP language based on a tuple space, to tackle this issue. In AspectKE*, aspects can enforce access control policies that depend on future behavior of running processes. One of the key language features is the predicates and functions that extract results of static program analysis, which are useful for defining security aspects that have to know about future behavior of a program. AspectKE* also provides a novel variable binding mechanism for pointcuts, so that pointcuts can uniformly specify join points based on both static and dynamic information about the program. Our implementation strategy performs fundamental static analysis at load-time, so as to retain runtime overheads minimal. We implemented a compiler for AspectKE*, and demonstrate usefulness of AspectKE* through a security aspect for a distributed chat system.

This thesis describes a level of communication among a class teacher, her pupils and the pupils themselves in a master class at a first stage, where the author works. The aim of the class teacher is to develop communicative competences that will lead to more effective communication in the class among the class teacher, her pupils and pupils themselves. The theoretical part gives a support to the practical part based on theoretical knowledge. It formulates specifics of pedagogical communication, features verbal communication, observes effective ways and barriers in communication. It submits tools by Personal and social education defining. The tools can reach expected outputs in communication defined in the National Curriculum and the Minimum Preventive Programme. The author introduces the teacher's personality and his skills as possible factors that affect the pupil's development. The practical part monitors the initial situation in the classroom. On the basis of a teacher action research the teacher wants to enhance communication efficiency. She uses the particular method of observation, reflection, Personal and social education techniques, audio and video recordings analysis and additionally verbal evaluation. She also relies on the application of the preventive programme. Data collection and the...

Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.