Formal and Automatic Security Policy Enforcement on Android Applications by Rewriting1

2021 ◽  
Author(s):  
Marwa Ziadia ◽  
Mohamed Mejri ◽  
Jaouhar Fattahi
Keyword(s):  
Formal Methods ◽  
Security Policy ◽  
Security Policies ◽  
Policy Enforcement ◽  
Android Application ◽  
System Specification ◽  
Policy Specification ◽  
Android Applications

With the wide variety of applications offered by Android, this system has been able to dominate the smartphone market. These applications provide all kinds of features and services that have become highly requested and welcomed by users. Besides, these applications represent risky vehicles for malware on Android devices. In this paper, we propose a novel formal technique to enforce the security of Android applications. We start off with an untrusted Android application and a security policy, and we end up in a new version of the application that behaves according to the policy. To ensure the correctness of results, we use formal methods in each step of the process, either in the system and the security policy specification or in the enforcement technique itself. The target application is reverse-engineered to its assembly-like code, Smali. An executable semantics called k-Smali was defined for this code using a language definitional framework, called k Framework. Security policies are specified in LTL-logic. The enforcement step consists of integrating the LTL formula in the k-Smali program using rewriting. It aims to rewrite the system specification automatically so that it satisfies the requested formula.

scholarly journals Security monitor inlining and certification for multithreaded Java

2014 ◽  
Vol 25 (3) ◽  
pp. 528-565 ◽  
Author(s):  
MADS DAM ◽  
BART JACOBS ◽  
ANDREAS LUNDBLAD ◽  
FRANK PIESSENS
Keyword(s):  
Security Policy ◽  
Security Policies ◽  
Policy Enforcement ◽  
Practical Application ◽  
Aspect Oriented Programming ◽  
Application Security ◽  
Fundamental Limitations ◽  
Java Bytecode ◽  
Verification Problem ◽  
Security Monitor

Security monitor inlining is a technique for security policy enforcement whereby monitor functionality is injected into application code in the style of aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). Such inliners are said to be correct. For sequential Java-like languages, inlining is well understood, and several provably correct inliners have been proposed. For multithreaded Java one difficulty is the need to maintain a shared monitor state. We show that this problem introduces fundamental limitations in the type of security policies that can be correctly enforced by inlining. A class of race-free policies is identified that precisely characterizes the inlineable policies by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete inliner for policies inside the class which is secure, conservative and transparent. The inliner is implemented for Java and applied to a number of practical application security policies. Finally, we discuss how certification in the style of proof-carrying code could be supported for inlined programs by using annotations to reduce a potentially complex verification problem for multithreaded Java bytecode to sequential verification of just the inlined code snippets.

Security Policies in Web Services

2010 ◽  
pp. 134-151
Author(s):  
Deepti Parachuri ◽  
Sudeep Mallick
Keyword(s):  
Web Services ◽  
Security Policy ◽  
Security Requirements ◽  
Security Policies ◽  
Future Trends ◽  
Security Measures ◽  
Computing Systems ◽  
Policy Specification ◽  
Basic Concepts

Security is of fundamental concern in computing systems. This chapter covers the role of security policies in Web services. First, it examines the importance of policies in web services and explains the WS-Policy standard. It also highlights the relation of WS-Policy with other WS-* specifications. Next, it covers different facets of security requirements in SOA implementations. Later, it examines the importance of security policies in web services. It also presents the basic concepts of WS-Security policy language. WS-Security policy specification specifies a standard way to define and publish security requirements in an extensible and interoperable way. A service provider makes use of security policy to publish the security measures implemented to protect the service. Security policies can also be made customizable to meet the security preferences of different consumers. Towards the end, it discusses about the governance of security polices and also future trends in security policies for web services.

scholarly journals RESPOnSE—A Framework for Enforcing Risk-Aware Security Policies in Constrained Dynamic Environments

Sensors ◽  
2020 ◽  
Vol 20 (10) ◽  
pp. 2960 ◽  
Author(s):  
Christina Michailidou ◽  
Vasileios Gkioulos ◽  
Andrii Shalaginov ◽  
Athanasios Rizos ◽  
Andrea Saracino
Keyword(s):  
Access Control ◽  
Security Policy ◽  
Dynamic Networks ◽  
Multicriteria Decision Making ◽  
Security Policies ◽  
Policy Enforcement ◽  
Role Based Access Control ◽  
Monitoring And Control ◽  
Attribute Based Access Control ◽  
Present Response

The enforcement of fine-grained access control policies in constrained dynamic networks can become a challenging task. The inherit constraints present in those networks, which result from the limitations of the edge devices in terms of power, computational capacity and storage, require an effective and efficient access control mechanism to be in place to provide suitable monitoring and control of actions and regulate the access over the resources. In this article, we present RESPOnSE, a framework for the specification and enforcement of security policies within such environments, where the computational burden is transferred to high-tier nodes, while low-tier nodes apply risk-aware policy enforcement. RESPOnSE builds on a combination of two widely used access control models, Attribute-Based Access Control and Role-Based Access Control, exploiting the benefits each one provides. Moreover, the proposed mechanism is founded on a compensatory multicriteria decision-making algorithm, based on the calculation of the Euclidean distance between the run-time values of the attributes present in the security policy and their ideal values, as those are specified within the established policy rules.

PENGEMBANGAN APLIKASI ANDROID BERBANTU SOFTWARE ISPRING SUITE SEBAGAI MEDIA PEMBELAJARAN EKONOMI MADRASAH ALIYAH MA’ARIF 9 KOTAGAJAH TAHUN PELAJARAN 2018/2019

2021 ◽  
Vol 1 (2) ◽  
pp. 175-187
Author(s):  
Novita Anggestia ◽  
Triani Ratnawuri ◽  
Meyta Pritandhari
Keyword(s):  
Learning Process ◽  
Development Model ◽  
Average Score ◽  
Application Software ◽  
Android Application ◽  
Design Development ◽  
Practical Research ◽  
Android Applications ◽  
Analysis Design ◽  
Made In

  Learning media is one of the needs that must be fulfilled in the learning process. The results of the pre-survey of learning media used in the Aliyah Ma'arif 9 Kotagajah Madrasah, researchers found several problems, namely the use of learning media that were less innovative in learning and the limitation of images in teaching books, worksheets and powerpoints so that students were not attracting attention in the learning process . So that learning media are needed that can attract the attention of students such as android applications, android application software assisted ispring suite as an economic learning media arranged concisely, clearly, and made in a practical form so that students are more interested and enthusiastic in learning and can understand the material. The development model used in this development is the ADDIE development model which consists of several stages, namely (Analysis, Design, Development, Implementation, and Evaluation). Based on the results of the development of android applications assisted by software ispring suite as an economic learning media it is known the results of recapitulation of data that have been carried out by learning media material experts on android applications with an average score of 86% included in the very feasible category and declared valid, the results of recapitulation from media experts with scores on average 87% fall into the category of very decent and declared valid. Furthermore, the practicality test by IPS X grade 1 students of Aliyah Ma'arif 9 Kotagajah gets an average score of 92.2% and falls into the very practical category so that it is declared practical. research shows that economic learning media using this android application is suitable for use in learning. Thus it can be concluded that the learning media of android applications are learning media that are valid and practical to be used in the learning process.

DIOXIN: runtime security policy enforcement of fog applications

2021 ◽  
Vol 12 (2) ◽  
pp. 126
Author(s):  
Enrico Russo ◽  
Luca Verderame ◽  
Alessandro Armando ◽  
Alessio Merlo
Keyword(s):  
Security Policy ◽  
Policy Enforcement

scholarly journals DAMPAK PEMANFAATAN APLIKASI ANDROID DALAM PEMBELAJARAN BANGUN RUANG

2018 ◽  
Vol 6 (2) ◽  
pp. 122-136
Author(s):  
Elisabeth Wiwik Sri Mulyani
Keyword(s):  
Action Research ◽  
Learning Process ◽  
Action Observation ◽  
Android Application ◽  
Learning Achievement ◽  
Learning Content ◽  
Learning Mathematics ◽  
Android Applications ◽  
The Impact ◽  
Planning Action

The purpose of this study was to know the impact of the utilization of android applications in learning mathematics in SMPN-1 Sragen. This classroom action research was conducted in two cycles,each cycle beginned with planning, action, observation, and reflection. The data in this study was the assessment of the learning process obtained from learners in the activity and assessment at the end of the cycle. Then, the data was analyzed to know whether the utilization of android application in teaching space has been successful or not. There was an increase in students' learning achievement in understanding mathematics after having utilized the android applications. Before the action, only 18 students (56.25%) completed their learning and increased to be 22 students (68.75%) on the first cycle. In the second cycle, the number of students completed their learning was 31 students (96.87%). The use of android application for class IX students B SMPN-1 Sragen had improved the students’ learning achievement. Before the action, the average knowledge of students was 75.16 and their average skill was 70.63. In the first cycle, the average knowledge of students is 78.59 and their average skills is 72.5. In the second cycle, of average knowledge 88.13 average skills 86.88. The conclusion, the utilization of android application in teaching the space learning content improved the students learning achievement. Teachers are suggested to utililize the android application or other appropriate media in learning-teaching activities.ABSTRAKFokus masalah yang menjadi pembahasan di dalam tulisan ini adalah dampak dari pemanfaatan aplikasi android dalam pembelajaran matematika tentang bangun ruang sisi lengkung di SMPN-1 Sragen. Tujuan penelitian ini adalah untuk mengetahui dampak dari pemanfaatan aplikasi android dalam pembelajaran matematika tentang bangun ruang sisi lengkung di SMPN-1 Sragen. Metode penelitian tindakan kelas ini dilaksanakan dengan dua siklus, di mana setiap siklus diawali dengan perencanaan, tindakan, observasi, dan refleksi. Data dalam penelitian ini berupa penilaian proses yang diperoleh dari peserta didik dalam beraktivitas dan penilaian pada akhir siklus. Kemudian, data dianalisis untuk memperoleh gambaran tentang berhasil-tidaknya pembelajaran yang telah dilakukan. Hasil penelitian menunjukkan ada peningkatan hasil belajar peserta didik dalam memahami bangun ruang sisi lengkung setelah belajar menggunakan aplikasi android. Sebelum tindakan, yang tuntas 18 peserta didik (56,25%), pada siklus pertama 22 peserta didik (68,75%). Pada siklus kedua, peserta didik yang tuntas belajarnya 31 orang (96,87%). Penggunaan aplikasi android pada peserta didik kelas IX B SMPN 1 Sragen terbukti dapat meningkatkan hasil belajar peserta didik. Sebelum tindakan, rata-rata pengetahuan 75,16 dan rata-rata keterampilan 70,63. Pada siklus pertama, rata-rata pengetahuan meningkat menjadi 78,59 dan rata-rata keterampilan 72,5. Kemudian, pada siklus kedua, rata-rata pengetahuan meningkat menjadi 88,13 dan rata-rata keterampilan meningkat menjadi 86,88. Simpulan dari penelitian ini adalah bahwa pemanfaatan aplikasi android pada materi bangun ruang meningkatkan hasil belajar peserta didik. Disarankan agar guru menggunakan aplikasi android atau media lain yang tepat dalam pembelajaran. 

Sign in / Sign up

Export Citation Format

Share Document