|
An app to demonstrate the risks of granting permissions in Android OS.
Michálek, J. ; Oujezský, V.
This article presents an application for demonstrating the risks of granting unsafe authorizations on Android devices. These permissions allow the application to access sensitive user data. The application uses practical examples to illustrate what user data can be abused by enabling permission. Nowadays, the security of user data is a growing topic. Therefore, mobile users themselves must be aware of the risks they expose themselves to by granting permissions.
|
|
Soothsharp: A C#-to-Viper translator
Hudeček, Petr ; Parízek, Pavel (advisor) ; Ježek, Pavel (referee)
Viper is a verification infrastructure developed at ETH Zurich. Using this infrastructure, programs written in the Viper language may be analyzed for correctness with respect to assertions and contracts. In this thesis, we develop a contracts library and a translator program that compiles C# code into the Viper language and thus allows it to be verified. A user may annotate their C# program with these contracts and then use the translator to determine its functional correctness. The translator supports most C# features, including types and arrays. It also integrates with Visual Studio, showing translation and verification errors to the user on-the-fly.
|
|
Security features of Android operating system and custom ROMs.
David, Adam ; Palovský, Radomír (advisor) ; Pavlíček, Luboš (referee)
Primary goal of this work is to analyze the Android operation system and its security. Thesis is divided in three parts: in the first one I will briefly describe the operation system and its development, in the second part I will analyze Androids security model and last part focuses on features of alternative ROMs, repositories and applications with emphasis on security and privacy. Despite Androids availability for plethora of various devices this thesis will focus on mobile phones.
|
|
The Rules of Normative Games
Svoboda, Vladimír
The paper considers the prospects of employing the framework of normative linguistic games proposed originally by D. Lewis for examination of logical features of expressions of prescriptive language.
|