This thesis focuses on the analysis of current information system of the selected points to its possible shortcomings and errors. Information obtained from the analyzes will lead to appropriate solutions to problems. The aim of the current system is customized to meet the needs of its users, so that the information system should be flexible, intuitive and clear

The aim of this dissertation thesis is to develop new methodology of information systems penetration testing based on analysis of current methodologies and the role of penetration tests in context of IS/IT governance. Integral part of this aim is evaluation of the methodology. The first part of the thesis is devoted to the presentation of history and current state of research in selected area, definiton of basic terms and introduction of role of the penetration tests. This part is followed by the review of relevant sources and comparative study of current methodologies with a goal to identify their weaknesses. Results from this study are further used as a basis for new methodology development. Classification of IS penetration tests types and testing scenarios are also included. The second part includes design of new methodology, at first its history, structure and principles are presented, then its framework is decribed in high level of detail. In the third part the reader can find (theoretical and practical) validation. The biggest scientific contribution is the methodology itself focused on managment of penetration tests (which is the area currently not sufficiently descibed). Secondary contribution is the extensive review and the comparative analysis of current methodologies. Contribution to the economic and technical (practical) application we can mainly see in the development of new methodology which enables companies to improve management of penetration tests (especially planning, operational management and implementation of countermeasures).

The mitigation of insider threats against databases is a challenging problem since insiders often have legitimate privileges to access sensitive data. Conventional security mechanisms, such as authentication and access control, are thus insufficient for the protection of databases against insider threats; such mechanisms need to be complemented with real-time anomaly detection techniques. Since the malicious activities aiming at stealing data may consist of multiple steps executed across temporal intervals, database anomaly detection is required to track users' actions across time in order to detect correlated actions that collectively indicate the occurrence of anomalies. The existing real-time anomaly detection techniques for databases can detect anomalies in the patterns of referencing the database entities, i.e., tables and columns, but are unable to detect the increase in the sizes of data retrieved by queries; neither can they detect changes in the users' data access frequencies. According to recent security reports, such changes are indicators of potential data misuse and may be the result of malicious intents for stealing or corrupting the data. In this thesis, we present techniques for monitoring database accesses and detecting anomalies that are considered early signs of data misuse by insiders. Our techniques are able to track the data retrieved by queries and sequences of queries, the frequencies of execution of periodic queries and the frequencies of referencing the database tuples and tables. We provide detailed algorithms and data structures that support the implementation of our techniques and the results of the evaluation of their implementation.<br>

<p>With the large number of Android apps available in app stores such as Google Play, it has become increasingly challenging to choose among the apps. The users generally select the apps based on the ratings and reviews of other users, or the recommendations from the app store. But it is very important to take the security into consideration while choosing an app with the increasing security and privacy concerns with mobile apps. This thesis proposes different ranking schemes for Android apps based on security apps evaluated from the static code analysis tools that are available. It proposes the ranking schemes based on the categories of evidences reported by the tools, based on the frequency of each category, and based on the severity of each evidence. The evidences are gathered, and rankings are generated based on the theory of Subjective Logic. In addition to these ranking schemes, the tools are themselves evaluated against the Ghera benchmark. Finally, this work proposes two additional schemes to combine the evidences from difference tools to provide a combined ranking.</p>

This thesis is focused on the information systems; it describes the available innovations applied on the established information systems. It describes the methods that are suitable for testing the effectiveness of the information systems. The practical part includes the current state of the chosen information system of a company, further it tests the effectiveness of the information system and finally it evaluates the received information and recommends the possible changes that would lead to the higher effectiveness of the work of the information system.

<div>Cellular networks are an indispensable part of a nation's critical infrastructure. They not only support functionality that are critical for our society as a whole (e.g., business, public-safety message dissemination) but also positively impact us at a more personal level by enabling applications that often improve our quality of life (e.g., navigation). Due to deployment constraints and backward compatibility issues, the various cellular protocol versions were not designed and deployed with a strong security and privacy focus. Because of their ubiquitous presence for connecting billions of users and use for critical applications, cellular networks are, however, lucrative attack targets of motivated and resourceful adversaries. </div><div><br></div><div></div><div>In this dissertation, we investigate the security and privacy of 4G LTE and 5G protocol designs and deployments. More precisely, we systematically identify design weaknesses and implementation oversights affecting the critical operations of the networks, and also design countermeasures to mitigate the identified vulnerabilities and attacks. Towards this goal, we developed a systematic model-based testing framework called LTEInspector. LTEInspector can be used to not only identify protocol design weaknesses but also deployment oversights. LTEInspector leverages the combined reasoning capabilities of a symbolic model checker and a cryptographic protocol verifier by combining them in a lazy fashion. We instantiated \system with three critical procedures (i.e., attach, detach, and paging) of 4G LTE. Our analysis uncovered 10 new exploitable vulnerabilities along with 9 prior attacks of 4G LTE all of which have been verified in a real testbed. Since identifying all classes of attacks with a unique framework like \system is nearly impossible, we show that it is possible to identify sophisticated security and privacy attacks by devising techniques specifically tailored for a particular protocol and by leveraging the findings of LTEInspector. As a case study, we analyzed the paging protocol of 4G LTE and the current version of 5G, and observed that by leveraging the findings from LTEInspector and other side-channel information and by using a probabilistic reasoning technique it is possible to mount sophisticated privacy attacks that can expose a victim device's coarse-grained location information and sensitive identifiers when the adversary is equipped only with the victim's phone number or other soft-identity (e.g., social networking profile). An analysis of LTEInspector's findings shows that the absence of broadcast authentication enables an adversary to mount a wide plethora of security and privacy attacks. We thus develop an attack-agnostic generic countermeasure that provides broadcast authentication without violating any common-sense deployment constraints. Finally, we design a practical countermeasure for mitigating the side-channel attacks in the paging procedure without breaking the backward compatibility.</div>

Alors que les systèmes embarqués sont de plus en plus nombreux, complexes, connectés et chargés de tâches critiques, la question de comment intégrer l'analyse précise de sécurité à la conception de systèmes embarqués doit trouver une réponse. Dans cette thèse, nous étudions comment les méthodes de vérification formelle automatiques peuvent aider les concepteurs de systèmes embarqués à évaluer l'impact des modifications logicielles et matérielles sur la sécurité des systèmes. Une des spécificités des systèmes embarqués est qu'ils sont décrits sous la forme de composants logiciels et matériels interagissant. Vérifier formellement de tels systèmes demande de prendre tous ces composants en compte. Nous proposons un exemple d'un tel système (basé sur Intel SGX) qui permet d'établir un canal sécurisé entre un périphérique et une application. Il est possible d'en vérifier un modèle de haut-niveau ou une implémentation bas-niveau. Ces deux niveaux diffèrent dans le degré d'intrication entre matériel et logiciel. Dans le premier cas, nous proposons une approche orientée modèle, à la fois au niveau partitionnement et conception logicielle, permettant une description à haut niveau d'abstraction du matériel et du logiciel et permettant une transformation de ces modèles en une spécification formelle sur laquelle une analyse de sécurité peut être effectuée avec l'outil ProVerif. Dans le second cas, nous considérons une implémentation logicielle et un modèle matériel plus concret pour effectuer des analyses de sécurité plus précises toujours avec ProVerif. / As embedded systems become more complex, more connected and more involved in critical tasks, the question of how strict security analysis can be performed during embedded system design needs to be thoroughly addressed. In this thesis, we study how automated formal verification can help embedded system designers in evaluating the impact of hardware and software modifications on the security of the whole system. One of the specificities of embedded system design-which is of particular interest for formal verification-is that the system under design is described as interacting hardware and software components. Formally verifying these systems requires taking both types of components into account. To illustrate this fact, we propose an example of a hardware/software co-design (based on Intel SGX) that provides a secure channel between a peripheral and an application. Formal verification can be performed on this system at different levels: from a high-level view (without describing the implementations) or from a low-level implementation. These two cases differ in terms of how tightly coupled the hardware and software components are. In the first case, we propose a model-based approach-for both the partitioning and software design phases- which enables us to describe software and hardware with high-level models and enables a transformation of these models into a formal specification which can be formally analyzed by the ProVerif tool. In the second case, we consider a software implementation and a more concrete

The OS (operating system) is the primary target of todays attacks. A single exploitable defect can be sufficient to break the security of the system and give fully control over all the software on the machine. Because current operating systems are too large to be defect free, the best approach to improve the system security is to reduce their code to more manageable levels. This work shows how the security-critical part of the OS, the so called TCB (Trusted Computing Base), can be reduced from millions to less than hundred thousand lines of code to achieve these security goals. Shrinking the software stack by more than an order of magnitude is an open challenge since no single technique can currently achieve this. We therefore followed a holistic approach and improved the design as well as implementation of several system layers starting with a new OS called NOVA. NOVA provides a small TCB for both newly written applications but also for legacy code running inside virtual machines. Virtualization is thereby the key technique to ensure that compatibility requirements will not increase the minimal TCB of our system. The main contribution of this work is to show how the virtual machine monitor for NOVA was implemented with significantly less lines of code without affecting the performance of its guest OS. To reduce the overall TCB of our system, other parts had to be improved as well. Additional contributions are the simplification of the OS debugging interface, the reduction of the boot stack and a new programming language called B1 that can be more easily compiled.

<div>Fuzzing is a simple yet effect approach to discover bugs by repeatedly testing the target system using randomly generated inputs. In this thesis, we identify several limitations in state-of-the-art fuzzing techniques: (1) the coverage wall issue , fuzzer-generated inputs cannot bypass complex sanity checks in the target programs and are unable to cover code paths protected by such checks; (2) inability to adapt to interfaces to inject fuzzer-generated inputs, one important example of such interface is the software/hardware interface between drivers and their devices; (3) dependency on code coverage feedback, this dependency makes it hard to apply fuzzing to targets where code coverage collection is challenging (due to proprietary components or special software design).</div><div><br></div><div><div>To address the coverage wall issue, we propose T-Fuzz, a novel approach to overcome the issue from a different angle: by removing sanity checks in the target program. T-Fuzz leverages a coverage-guided fuzzer to generate inputs. Whenever the coverage wall is reached, a light-weight, dynamic tracing based technique detects the input checks that the fuzzer-generated inputs fail. These checks are then removed from the target program. Fuzzing then continues on the transformed program, allowing the code protected by the removed checks to be triggered and potential bugs discovered. Fuzzing transformed programs to find bugs poses two challenges: (1) removal of checks leads to over-approximation and false positives, and (2) even for true bugs, the crashing input on the transformed program may not trigger the bug in the original program. As an auxiliary post-processing step, T-Fuzz leverages a symbolic execution-based approach to filter out false positives and reproduce true bugs in the original program.</div></div><div><br></div><div><div>By transforming the program as well as mutating the input, T-Fuzz covers more code and finds more true bugs than any existing technique. We have evaluated T-Fuzz on the DARPA Cyber Grand Challenge dataset, LAVA-M dataset and 4 real-world programs (pngfix, tiffinfo, magick and pdftohtml). For the CGC dataset, T-Fuzz finds bugs in 166 binaries, Driller in 121, and AFL in 105. In addition, we found 4 new bugs in previously-fuzzed programs and libraries.</div></div><div><br></div><div><div>To address the inability to adapt to inferfaces, we propose USBFuzz. We target the USB interface, fuzzing the software/hardware barrier. USBFuzz uses device emulation</div><div>to inject fuzzer-generated input to drivers under test, and applies coverage-guided fuzzing to device drivers if code coverage collection is supported from the kernel. In its core, USBFuzz emulates an special USB device that provides data to the device driver (when it performs IO operations). This allows us to fuzz the input space of drivers from the device’s perspective, an angle that is difficult to achieve with real hardware. USBFuzz discovered 53 bugs in Linux (out of which 37 are new, and 36 are memory bugs of high security impact, potentially allowing arbitrary read or write in the kernel address space), one bug in FreeBSD, four bugs (resulting in Blue Screens of Death) in Windows and three bugs (two causing an unplanned restart, one freezing the system) in MacOS.</div></div><div><br></div><div><div>To break the dependency on code coverage feedback, we propose WebGLFuzzer. To fuzz the WebGL interface (a set of JavaScript APIs in browsers allowing high performance graphics rendering taking advantage of GPU acceleration on the device), where code coverage collection is challenging, we introduce WebGLFuzzer, which internally uses a log guided fuzzing technique. WebGLFuzzer is not dependent on code coverage feedback, but instead, makes use of the log messages emitted by browsers to guide its input mutation. Compared with coverage guided fuzzing, our log guided fuzzing technique is able to perform more meaningful mutation under the guidance of the log message. To this end, WebGLFuzzer uses static analysis to identify which argument to mutate or which API call to insert to the current program to fix the internal WebGL program state given a log message emitted by the browser. WebGLFuzzer is under evaluation and so far, it has found 6 bugs, one of which is able to freeze the X-Server.</div></div>

Robotic aerial vehicles (RAVs) have been increasingly deployed in various areas (e.g., commercial, military, scientific, and entertainment). However, RAVs’ security and safety issues could not only arise from either of the “cyber” domain (e.g., control software) and “physical” domain (e.g., vehicle control model) but also stem in their interplay. Unfortunately, existing work had focused mainly on either the “cyber-centric” or “control-centric” approaches. However, such a single-domain focus could overlook the security threats caused by the interplay between the cyber and physical domains. <br>In this thesis, we present cyber-physical analysis and hardening to secure RAV controllers. Through a combination of program analysis and vehicle control modeling, we first developed novel techniques to (1) connect both cyber and physical domains and then (2) analyze individual domains and their interplay. Specifically, we describe how to detect bugs after RAV accidents using provenance (Mayday), how to proactively find bugs using fuzzing (RVFuzzer), and how to patch vulnerable firmware using binary patching (DisPatch). As a result, we have found 91 new bugs in modern RAV control programs, and their developers confirmed 32 cases and patch 11 cases.