scholarly journals Formal Verification of a Mandatory Integrity Control Model for the KasperskyOS Operating System

2020 ◽  
Vol 32 (6) ◽  
pp. 31-48
Author(s):  
Vladimir Sergeevich Burenkov
Keyword(s):  
Operating System ◽  
Formal Verification ◽  
Operating Systems ◽  
Trusted Computing ◽  
Control Model ◽  
Discrete Mathematics ◽  
Active Components ◽  
Access To Resources ◽  
Trusted Computing Base ◽  
Automated Proof

Models of mandatory integrity control in operating systems usually restrict accesses of active components of a system to passive ones and represent the accesses directly. This is suitable in case of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, due to the sheer complexity of such components, it is extremely nontrivial to prove such a model to be adequate to the real system. KasperskyOS is a microkernel operating system that organizes access to resources via components that are not necessarily part of the trusted computing base. KasperskyOS implements a specifically developed mandatory integrity control model that takes such components into account. This paper formalizes the model and describes the process of automated proof of the model’s properties. For formalization, we use the Event-B language. We clarify parts specific to Event-B to make our presentation accessible to professionals familiar with discrete mathematics but not necessarily with Event-B. We reflect on the proof experience obtained in the Rodin platform.

scholarly journals Formal Verification of a Mandatory Integrity Control Model for the KasperskyOS Operating System

2020 ◽  
Vol 32 (6) ◽  
pp. 31-48
Author(s):  
Vladimir Sergeevich Burenkov
Keyword(s):  
Operating System ◽  
Formal Verification ◽  
Operating Systems ◽  
Trusted Computing ◽  
Control Model ◽  
Discrete Mathematics ◽  
Active Components ◽  
Access To Resources ◽  
Trusted Computing Base ◽  
Automated Proof

Models of mandatory integrity control in operating systems usually restrict accesses of active components of a system to passive ones and represent the accesses directly. This is suitable in case of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, due to the sheer complexity of such components, it is extremely nontrivial to prove such a model to be adequate to the real system. KasperskyOS is a microkernel operating system that organizes access to resources via components that are not necessarily part of the trusted computing base. KasperskyOS implements a specifically developed mandatory integrity control model that takes such components into account. This paper formalizes the model and describes the process of automated proof of the model’s properties. For formalization, we use the Event-B language. We clarify parts specific to Event-B to make our presentation accessible to professionals familiar with discrete mathematics but not necessarily with Event-B. We reflect on the proof experience obtained in the Rodin platform.

scholarly journals An Adaptive Scheduler for Real-Time Operating Systems to Extend WSN Nodes Lifetime

2018 ◽  
Vol 2018 ◽  
pp. 1-10 ◽  
Author(s):  
Roberto Rodriguez-Zurrunero ◽  
Ramiro Utrilla ◽  
Elena Romero ◽  
Alvaro Araujo
Keyword(s):  
Operating System ◽  
Real Time ◽  
Operating Systems ◽  
Research Area ◽  
Rechargeable Batteries ◽  
Wireless Sensor ◽  
Portable Devices ◽  
Wireless Devices ◽  
Changing Environments ◽  
Tasks Scheduling

Wireless Sensor Networks (WSNs) are a growing research area as a large of number portable devices are being developed. This fact makes operating systems (OS) useful to homogenize the development of these devices, to reduce design times, and to provide tools for developing complex applications. This work presents an operating system scheduler for resource-constraint wireless devices, which adapts the tasks scheduling in changing environments. The proposed adaptive scheduler allows dynamically delaying the execution of low priority tasks while maintaining real-time capabilities on high priority ones. Therefore, the scheduler is useful in nodes with rechargeable batteries, as it reduces its energy consumption when battery level is low, by delaying the least critical tasks. The adaptive scheduler has been implemented and tested in real nodes, and the results show that the nodes lifetime could be increased up to 70% in some scenarios at the expense of increasing latency of low priority tasks.

INSTALASI SISTEM OPERASI BERBASIS WINDOWS 10 PADA SEKOLAH MAN KISARAN

2020 ◽  
Vol 3 (2) ◽  
pp. 163-168
Author(s):  
Ruri Ashari Dalimunthe ◽  
Riki Andri Yusda ◽  
William Ramdhan
Keyword(s):  
Operating System ◽  
Community Service ◽  
Operating Systems ◽  
Direct Observation ◽  
Computer Lab ◽  
Service Activities ◽  
Computer Labs ◽  
At Home

Abstract: Community service activities entitled "Installation of Operating Systems Based on Windows 10" aims to provide information to students from MAN Asahan about Installing Windows Operating Systems. The method used in this activity is a direct observation of the MAN Asahan school by watching and analyzing the problems or troubleshooting that occurs at the Computer Lab at MAN Asahan. In addition, information on problems in the computer Labs of the school was also carried out by a team of lecturers as the perpetrators of this community service by way of direct interviews with the Teachers and employees who served in the Computer Lab of the MAN Asahan school. The end result of this dedication is how students can repair computers, as well as troubleshooting that occurs on school computers and computers at home, can be overcome alone without having to use computer repair services.Keywords: installation; operating system; Windows 10 Abstrak: Kegiatan pengabdian kepada masyarakat yang diberi judul “Instalasi Sistem Operasi Berbasis Windows 10” bertujuan untuk memberikan informasi kepada siswa dan siswi MAN Asahan tentang Instalasi Sistem Operasi Windows. Metode yang digunakan dalam kegiatan ini adalah observasi langsung ke sekolah MAN Asahan dengan melihat serta menganalisa permasalahan ataupun troubleshooting yang terjadi pada Laboratorium Komputer disekolah MAN Asahan. Selain itu, Informasi permasalahan pada komputer Lab sekolah juga dilakukan tim dosen selaku pelaku kegiatan pengabdian ini dengan cara wawancara langsung kepada Guru dan pegawai yang bertugas di Lab Komputer sekolah MAN Asahan. Hasil akhir dari pengabdian ini adalah bagaimana siswa dan siswi dapat memperbaiki komputer serta troubleshooting yang terjadi pada komputer sekolah maupun komputer dirumah dapat teratasi sendiri tanpa harus memakai jasa perbaikan komputer. Kata kunci: instalasi; sistem operasi;  windows 10

DEVS OS (Discrete Even Visualization and Simulation Operating System)

2018 ◽  
Author(s):  
Adnan Hajar
Keyword(s):  
Operating System ◽  
Operating Systems ◽  
Scheduling Algorithm ◽  
The Novel ◽  
Priority Scheduling ◽  
First Come First Serve ◽  
Multiple Cycles ◽  
Visualization And Simulation ◽  
Traditional Approaches

The use of traditional approaches to teach Operating Systems usually lacks the visual aspect. The following research investigates the novel use of DEVS (Discrete Even Visualization and Simulation) in simulating the operation of an operating system. Cd boost++ was the framework of choice for this project. The simulation successfully mimicked the work of an operating system by simulating multiple cycles of program requests. This simulation is capable of further enhance the explanation of how an operating system works. The cases studied in this work include: 1- two processes running concurrently doing multiple IO’s, 2-four processes running concurrently based on a first come first serve scheduling algorithm, and 3- 20 processes running concurrently using highest priority scheduling algorithm. Output observation of the last case show promising results of successful use of DEVS and cd boost++ as a framework to build an operating system.

scholarly journals Threats and Vulnerabilities to IoT End Devices Architecture and suggested remedies

2020 ◽  
Vol 8 (6) ◽  
pp. 5712-5718
Keyword(s):  
Decision Making ◽  
Internet Of Things ◽  
Data Processing ◽  
Trusted Computing ◽  
External World ◽  
Security Threats ◽  
Iot Applications ◽  
Trusted Computing Base ◽  
Chain Of Trust ◽  
New Challenges

Due to decentralization of Internet of Things(IoT) applications and anything, anytime, anywhere connectivity has increased burden of data processing and decision making at IoT end devices. This overhead initiated new bugs and vulnerabilities thus security threats are emerging and presenting new challenges on these end devices. IoT End Devices rely on Trusted Execution Environments (TEEs) by implementing Root of trust (RoT) as soon as power is on thus forming Chain of trust (CoT) to ensure authenticity, integrity and confidentiality of every bit and byte of Trusted Computing Base (TCB) but due to un-trusted external world connectivity and security flaws such as Spectre and meltdown vulnerabilities present in the TCB of TEE has made CoT unstable and whole TEE are being misutilized. This paper suggests remedial solutions for the threats arising due to bugs and vulnerabilities present in the different components of TCB so as to ensure the stable CoT resulting into robust TEE.

scholarly journals Android Application Development

2021 ◽  
Vol 9 (VI) ◽  
pp. 3188-3192
Author(s):  
Ritu Sharma
Keyword(s):  
Operating System ◽  
Digital Media ◽  
Operating Systems ◽  
Mobile Apps ◽  
Video Recording ◽  
Weather Forecast ◽  
Smart Phones ◽  
Human Beings ◽  
Application Development ◽  
Audio Video

Technology is being used and improved by human beings over a long period of time now and Smartphones is one of them. Smart Phones contain touch screen, built in keyboard, high resolution camera, front side camera for video conferencing, etc. They are used for making and receiving calls, sending and receiving messages, accessing the Internet, digital media, incorporating audio/video recording etc. Different smart phones have different operating systems and mobile applications are developed for each operating system in smart phones, tablet or mobile phones, in order to serve the needs of the user. These apps are either preinstalled or downloadable from online app market that can do almost everything. Apps make a mobile be like a portable computer having multi core processors, gigabytes of memory and a real operating system. Originally mobile apps were made available for only calling, messaging and informational purposes like calendar, weather forecast, e- mail, etc. With improvement in technology and increase in user demands, developers started making apps for other purposes like games, banking, video chats etc. Some apps are also used to present data in the same format as on a computer website and also allow you to download content that you can use when there is no Internet. There are many apps available in market today for different Operating Systems in which Android is having the maximum market share these days.

scholarly journals The Impact of Operating System on Bandwidth in Open VPN Technology

2016 ◽  
Vol 13 (1) ◽  
pp. 204-211
Author(s):  
Baghdad Science Journal
Keyword(s):  
Operating System ◽  
Operating Systems ◽  
Data Privacy ◽  
The Internet ◽  
Sensitive Data ◽  
Privacy And Security ◽  
Basic Source ◽  
Basic Functions ◽  
And Performance ◽  
The Impact

The internet is a basic source of information for many specialities and uses. Such information includes sensitive data whose retrieval has been one of the basic functions of the internet. In order to protect the information from falling into the hands of an intruder, a VPN has been established. Through VPN, data privacy and security can be provided. Two main technologies of VPN are to be discussed; IPSec and Open VPN. The complexity of IPSec makes the OpenVPN the best due to the latter’s portability and flexibility to use in many operating systems. In the LAN, VPN can be implemented through Open VPN to establish a double privacy layer(privacy inside privacy). The specific subnet will be used in this paper. The key and certificate will be generated by the server. An authentication and key exchange will be based on standard protocol SSL/TLS. Various operating systems from open source and windows will be used. Each operating system uses a different hardware specification. Tools such as tcpdump and jperf will be used to verify and measure the connectivity and performance. OpenVPN in the LAN is based on the type of operating system, portability and straightforward implementation. The bandwidth which is captured in this experiment is influenced by the operating system rather than the memory and capacity of the hard disk. Relationship and interoperability between each peer and server will be discussed. At the same time privacy for the user in the LAN can be introduced with a minimum specification.

A Methodology for Appropriate Testing When Data is Heterogeneous Using EXCEL

2016 ◽  
Vol 4 (1) ◽  
pp. 54-66
Author(s):  
Nguyen Khanh ◽  
Jimin Lee ◽  
Susan Reiser ◽  
Donna Parsons ◽  
Sara Russell ◽  
...  
Keyword(s):  
Operating System ◽  
Programming Languages ◽  
Operating Systems ◽  
Degrees Of Freedom ◽  
Heterogeneous Data ◽  
Data Sets ◽  
Social Scientists ◽  
Unequal Variances ◽  
Data Volume ◽  
Nonparametric Techniques

A Methodology for Appropriate Testing When Data is Heterogeneous was originally published and copy written in the mid-1990s in Turbo Pascal and a 16-bit operating system.  While working on an ergonomic dissertation (Yearout, 1987), the author determined that the perceptual lighting preference data was heterogeneous and not normal.  Drs. Milliken and Johnson, the authors of Analysis of Messy Data Volume I: Designed Experiments (1989), advised that Satterthwaite’s Approximation with Bonferroni’s Adjustment to correct for pairwise error be used to analyze the heterogeneous data. This technique of applying linear combinations with adjusted degrees of freedom allowed the use of t-Table criteria to make group comparisons without using standard nonparametric techniques.  Thus data with unequal variances and unequal sample sizes could be analyzed without losing valuable information.  Variances to the 4th power were so large that they could not be reentered into basic calculators.  The solution was to develop an original software package which was written in Turbo Pascal on a 7 ¼ inch disk 16-bit operating system.  Current operating systems of 32 and 64 bits and more efficient programming languages have made the software obsolete and unusable. Using the old system could result either in many returns being incorrect or the system terminating.  The purpose of this research was to develop a spreadsheet algorithm with multiple interactive EXCEL worksheets that will efficiently apply Satterthwaite’s Approximation with Bonferroni’s Adjustment to solve the messy data problem.  To ensure that the pedagogy is accurate, the resulting package was successfully tested in the classroom with academically diverse students.  A comparison between this technique and EXCEL’s Add-Ins Analysis ToolPak for a t-test Two-Sample Assuming Unequal Variances was conducted using several different data sets.  The results of this comparison were that the EXCEL Add-Ins returned incorrect significant differences.  Engineers, ergonomists, psychologists, and social scientists will find the developed program very useful. A major benefit is that spreadsheets will continue to be current regardless of evolving operating systems’ status.

Sign in / Sign up

Export Citation Format

Share Document