Visible to the public Biblio

Filters: Keyword is Ports (Computers)  [Clear All Filters]
2023-06-16
Yang, Di, Wang, Lianfa, Zhang, Yufeng.  2022.  Research on the Application of Computer Big Data Technology in the Health Monitoring of the Bridge Body of Cross-river Bridge. 2022 IEEE Asia-Pacific Conference on Image Processing, Electronics and Computers (IPEC). :1516—1520.
This article proposes a health monitoring system platform for cross-river bridges based on big data. The system can realize regionalized bridge operation and maintenance management. The system has functions such as registration modification and deletion of sensor equipment, user registration modification and deletion, real-time display and storage of sensor monitoring data, and evaluation and early warning of bridge structure safety. The sensor is connected to the lower computer through the serial port, analog signal, fiber grating signal, etc. The lower computer converts a variety of signals into digital signals through the single-chip A/D sampling and demodulator, etc., and transmits it to the upper computer through the serial port. The upper computer uses ARMCortex-A9 Run the main program to realize multi-threaded network communication. The system platform is to test the validity of the model, and a variety of model verification methods are used for evaluation to ensure the reliability of the big data analysis method.
2023-01-13
Pali, Isha, Amin, Ruhul.  2022.  PortSec: Securing Port Knocking System using Sequence Mechanism in SDN Environment. 2022 International Wireless Communications and Mobile Computing (IWCMC). :1009—1014.
Port knocking provides an added layer of security on top of the existing security systems of a network. A predefined port knocking sequence is used to open the ports, which are closed by the firewall by default. The server determines the valid request if the knocking sequence is correct and opens the desired port. However, this sequence poses a security threat due to its static nature. This paper presents the port knock sequence-based communication protocol in the Software Defined network (SDN). It provides better management by separating the control plane and data plane. At the same time, it causes a communication overhead between the switches and the controller. To avoid this overhead, we are using the port knocking concept in the data plane without any involvement of the SDN controller. This study proposes three port knock sequence-based protocols (static, partial dynamic, and dynamic) in the data plane. To test the protocol in SDN environment, the P4 implementation of the underlying model is done in the BMV2 (behavioral model version 2) virtual switch. To check the security of the protocols, an informal security analysis is performed, which shows that the proposed protocols are secured to be implemented in the SDN data plane.
2022-12-01
Kao, Chia-Nan, Chang, Yung-Cheng, Huang, Nen-Fu, Salim S, I, Liao, I.-Ju, Liu, Rong-Tai, Hung, Hsien-Wei.  2015.  A predictive zero-day network defense using long-term port-scan recording. 2015 IEEE Conference on Communications and Network Security (CNS). :695—696.
Zero-day attack is a critical network attack. The zero-day attack period (ZDAP) is the period from the release of malware/exploit until a patch becomes available. IDS/IPS cannot effectively block zero-day attacks because they use pattern-based signatures in general. This paper proposes a Prophetic Defender (PD) by which ZDAP can be minimized. Prior to actual attack, hackers scan networks to identify hosts with vulnerable ports. If this port scanning can be detected early, zero-day attacks will become detectable. PD architecture makes use of a honeypot-based pseudo server deployed to detect malicious port scans. A port-scanning honeypot was operated by us in 6 years from 2009 to 2015. By analyzing the 6-year port-scanning log data, we understand that PD is effective for detecting and blocking zero-day attacks. The block rate of the proposed architecture is 98.5%.
2022-04-20
Deschamps, Henrick, Cappello, Gerlando, Cardoso, Janette, Siron, Pierre.  2017.  Toward a Formalism to Study the Scheduling of Cyber-Physical Systems Simulations. 2017 IEEE/ACM 21st International Symposium on Distributed Simulation and Real Time Applications (DS-RT). :1–8.
This paper presents ongoing work on the formalism of Cyber-Physical Systems (CPS) simulations. These systems are distributed real-time systems, and their simulations might be distributed or not. In this paper, we propose a model to describe the modular components forming a simulation of a CPS. The main goal is to introduce a model of generic simulation distributed architecture, on which we are able to execute a logical architecture of simulation. This architecture of simulation allows the expression of structural and behavioural constraints on the simulation, abstracting its execution. We will propose two implementations of the execution architecture based on generic architectures of distributed simulation: $\cdot$ The High Level Architecture (HLA), an IEEE standard for distributed simulation, and one of its open-source implementation of RunTime Infrastructure (RTI): CERTI. $\cdot$ The Distributed Simulation Scheduler (DSS), an Airbus framework scheduling predefined models. Finally, we present the initial results obtained applying our formalism to the open-source case study from the ROSACE case study.
2022-03-08
Mizushiro, Takuya, Kitasuka, Teruaki.  2021.  Porting Caching Functions to Named Data Networking Forwarding Daemon (NFD). 2021 Ninth International Symposium on Computing and Networking Workshops (CANDARW). :73–76.
The purpose of using the Internet has changed from "connecting to computers" to "acquiring content". So, the ICN (Information Centric Network) has been proposed to fit this purpose. In this research, we focus on the architecture of NDN (named data networking). The NFD (NDN forwarding daemon) is a network forwarder that implements the NDN protocol. The ndnSIM is a simulator of NDN. From ndnSIM version 2.8, a part of content store implementation has been removed from the simulator and it becomes to use content store implementation of NFD. In this poster, we select two caching functions, probabilistic caching and expired deletion, which are removed from ndnSIM 2.8 and not included in NFD. We port these functions to NFD for a more practical implementation. Under a certain network, we were able to confirm that previous and ported functions provided equivalent functions. It was also possible to simulate in version ndnSIM 2.8 using the ported functions.
Grzelak, Bartosz, Keim, Martin, Pogiel, Artur, Rajski, Janusz, Tyszer, Jerzy.  2021.  Convolutional Compaction-Based MRAM Fault Diagnosis. 2021 IEEE European Test Symposium (ETS). :1–6.
Spin-transfer torque magnetoresistive random-access memories (STT-MRAMs) are gradually superseding conventional SRAMs as last-level cache in System-on-Chip designs. Their manufacturing process includes trimming a reference resistance in STT-MRAM modules to reliably determine the logic values of 0 and 1 during read operations. Typically, an on-chip trimming routine consists of multiple runs of a test algorithm with different settings of a trimming port. It may inherently produce a large number of mismatches. Diagnosis of such a sizeable volume of errors by means of existing memory built-in self-test (MBIST) schemes is either infeasible or a time-consuming and expensive process. In this paper, we propose a new memory fault diagnosis scheme capable of handling STT-MRAM-specific error rates in an efficient manner. It relies on a convolutional reduction of memory outputs and continuous shifting of the resultant data to a tester through a few output channels that are typically available in designs using an on-chip test compression technology, such as the embedded deterministic test. It is shown that processing the STT-MRAM output by using a convolutional compactor is a preferable solution for this type of applications, as it provides a high diagnostic resolution while incurring a low hardware overhead over traditional MBIST logic.
2020-01-20
Musca, Constantin, Mirica, Emma, Deaconescu, Razvan.  2013.  Detecting and Analyzing Zero-Day Attacks Using Honeypots. 2013 19th International Conference on Control Systems and Computer Science. :543–548.

Computer networks are overwhelmed by self propagating malware (worms, viruses, trojans). Although the number of security vulnerabilities grows every day, not the same thing can be said about the number of defense methods. But the most delicate problem in the information security domain remains detecting unknown attacks known as zero-day attacks. This paper presents methods for isolating the malicious traffic by using a honeypot system and analyzing it in order to automatically generate attack signatures for the Snort intrusion detection/prevention system. The honeypot is deployed as a virtual machine and its job is to log as much information as it can about the attacks. Then, using a protected machine, the logs are collected remotely, through a safe connection, for analysis. The challenge is to mitigate the risk we are exposed to and at the same time search for unknown attacks.

2018-11-14
Sakumoto, S., Kanaoka, A..  2017.  Improvement of Privacy Preserved Rule-Based Risk Analysis via Secure Multi-Party Computation. 2017 12th Asia Joint Conference on Information Security (AsiaJCIS). :15–22.

Currently, when companies conduct risk analysis of own networks and systems, it is common to outsource risk analysis to third-party experts. At that time, the company passes the information used for risk analysis including confidential information such as network configuration to third-party expert. It raises the risk of leakage and abuse of confidential information. Therefore, a method of risk analysis by using secure computation without passing confidential information of company has been proposed. Although Liu's method have firstly achieved secure risk analysis method using multiparty computation and attack tree analysis, it has several problems to be practical. In this paper, improvement of secure risk analysis method is proposed. It can dynamically reduce compilation time, enhance scale of target network and system without increasing execution time. Experimental work is carried out by prototype implementation. As a result, we achieved improved performance in compile time and enhance scale of target with equivalent performance on execution time.

2018-06-11
Zhang, X., Li, R., Zhao, W., Wu, R..  2017.  Detection of malicious nodes in NDN VANET for Interest Packet Popple Broadcast Diffusion Attack. 2017 11th IEEE International Conference on Anti-counterfeiting, Security, and Identification (ASID). :114–118.

As one of the next generation network architectures, Named Data Networking(NDN) which features location-independent addressing and content caching makes it more suitable to be deployed into Vehicular Ad-hoc Network(VANET). However, a new attack pattern is found when NDN and VANET combine. This new attack is Interest Packet Popple Broadcast Diffusion Attack (PBDA). There is no mitigation strategies to mitigate PBDA. In this paper a mitigation strategies called RVMS based on node reputation value (RV) is proposed to detect malicious nodes. The node calculates the neighbor node RV by direct and indirect RV evaluation and uses Markov chain predict the current RV state of the neighbor node according to its historical RV. The RV state is used to decide whether to discard the interest packet. Finally, the effectiveness of the RVMS is verified through modeling and experiment. The experimental results show that the RVMS can mitigate PBDA.

Jung, M. Y., Jang, J. W..  2017.  Data management and searching system and method to provide increased security for IoT platform. 2017 International Conference on Information and Communication Technology Convergence (ICTC). :873–878.

Existing data management and searching system for Internet of Things uses centralized database. For this reason, security vulnerabilities are found in this system which consists of server such as IP spoofing, single point of failure and Sybil attack. This paper proposes data management system is based on blockchain which ensures security by using ECDSA digital signature and SHA-256 hash function. Location that is indicated as IP address of data owner and data name are transcribed in block which is included in the blockchain. Furthermore, we devise data manegement and searching method through analyzing block hash value. By using security properties of blockchain such as authentication, non-repudiation and data integrity, this system has advantage of security comparing to previous data management and searching system using centralized database or P2P networks.

2018-05-24
Zhongchao, W., Ligang, H., Baojun, T., Wensi, W., Jinhui, W..  2017.  Design and Verification of a Novel IoT Node Protocol. 2017 13th IEEE International Conference on Electronic Measurement Instruments (ICEMI). :201–205.

The IoT node works mostly in a specific scenario, and executes the fixed program. In order to make it suitable for more scenarios, this paper introduces a kind of the IoT node, which can change program at any time. And this node has intelligent and dynamic reconfigurable features. Then, a transport protocol is proposed. It enables this node to work in different scenarios and perform corresponding program. Finally, we use Verilog to design and FPGA to verify. The result shows that this protocol is feasible. It also offers a novel way of the IoT.

2018-05-09
Aliyu, A. L., Bull, P., Abdallah, A..  2017.  A Trust Management Framework for Network Applications within an SDN Environment. 2017 31st International Conference on Advanced Information Networking and Applications Workshops (WAINA). :93–98.

Software Defined Networking (SDN) is an emerging paradigm that changes the way networks are managed by separating the control plane from data plane and making networks programmable. The separation brings about flexibility, automation, orchestration and offers savings in both capital and operational expenditure. Despite all the advantages offered by SDN it introduces new threats that did not exist before or were harder to exploit in traditional networks, making network penetration potentially easier. One of the key threat to SDN is the authentication and authorisation of network applications that control network behaviour (unlike the traditional network where network devices like routers and switches are autonomous and run proprietary software and protocols to control the network). This paper proposes a mechanism that helps the control layer authenticate network applications and set authorisation permissions that constrict manipulation of network resources.

Dridi, M., Rubini, S., Lallali, M., Florez, M. J. S., Singhoff, F., Diguet, J. P..  2017.  DAS: An Efficient NoC Router for Mixed-Criticality Real-Time Systems. 2017 IEEE International Conference on Computer Design (ICCD). :229–232.

Mixed-Criticality Systems (MCS) are real-time systems characterized by two or more distinct levels of criticality. In MCS, it is imperative that high-critical flows meet their deadlines while low critical flows can tolerate some delays. Sharing resources between flows in Network-On-Chip (NoC) can lead to different unpredictable latencies and subsequently complicate the implementation of MCS in many-core architectures. This paper proposes a new virtual channel router designed for MCS deployed over NoCs. The first objective of this router is to reduce the worst-case communication latency of high-critical flows. The second aim is to improve the network use rate and reduce the communication latency for low-critical flows. The proposed router, called DAS (Double Arbiter and Switching router), jointly uses Wormhole and Store And Forward techniques for low and high-critical flows respectively. Simulations with a cycle-accurate SystemC NoC simulator show that, with a 15% network use rate, the communication delay of high-critical flows is reduced by 80% while communication delay of low-critical flow is increased by 18% compared to usual solutions based on routers with multiple virtual channels.

Mahajan, V., Peddoju, S. K..  2017.  Integration of Network Intrusion Detection Systems and Honeypot Networks for Cloud Security. 2017 International Conference on Computing, Communication and Automation (ICCCA). :829–834.

With an aim of provisioning fast, reliable and low cost services to the users, the cloud-computing technology has progressed leaps and bounds. But, adjacent to its development is ever increasing ability of malicious users to compromise its security from outside as well as inside. The Network Intrusion Detection System (NIDS) techniques has gone a long way in detection of known and unknown attacks. The methods of detection of intrusion and deployment of NIDS in cloud environment are dependent on the type of services being rendered by the cloud. It is also important that the cloud administrator is able to determine the malicious intensions of the attackers and various methods of attack. In this paper, we carry out the integration of NIDS module and Honeypot Networks in Cloud environment with objective to mitigate the known and unknown attacks. We also propose method to generate and update signatures from information derived from the proposed integrated model. Using sandboxing environment, we perform dynamic malware analysis of binaries to derive conclusive evidence of malicious attacks.

Andy, S., Rahardjo, B., Hanindhito, B..  2017.  Attack scenarios and security analysis of MQTT communication protocol in IoT system. 2017 4th International Conference on Electrical Engineering, Computer Science and Informatics (EECSI). :1–6.
Various communication protocols are currently used in the Internet of Things (IoT) devices. One of the protocols that are already standardized by ISO is MQTT protocol (ISO / IEC 20922: 2016). Many IoT developers use this protocol because of its minimal bandwidth requirement and low memory consumption. Sometimes, IoT device sends confidential data that should only be accessed by authorized people or devices. Unfortunately, the MQTT protocol only provides authentication for the security mechanism which, by default, does not encrypt the data in transit thus data privacy, authentication, and data integrity become problems in MQTT implementation. This paper discusses several reasons on why there are many IoT system that does not implement adequate security mechanism. Next, it also demonstrates and analyzes how we can attack this protocol easily using several attack scenarios. Finally, after the vulnerabilities of this protocol have been examined, we can improve our security awareness especially in MQTT protocol and then implement security mechanism in our MQTT system to prevent such attack.
Jonsdottir, G., Wood, D., Doshi, R..  2017.  IoT network monitor. 2017 IEEE MIT Undergraduate Research Technology Conference (URTC). :1–5.
IoT Network Monitor is an intuitive and user-friendly interface for consumers to visualize vulnerabilities of IoT devices in their home. Running on a Raspberry Pi configured as a router, the IoT Network Monitor analyzes the traffic of connected devices in three ways. First, it detects devices with default passwords exploited by previous attacks such as the Mirai Botnet, changes default device passwords to randomly generated 12 character strings, and reports the new passwords to the user. Second, it conducts deep packet analysis on the network data from each device and notifies the user of potentially sensitive personal information that is being transmitted in cleartext. Lastly, it detects botnet traffic originating from an IoT device connected to the network and instructs the user to disconnect the device if it has been hacked. The user-friendly IoT Network Monitor will enable homeowners to maintain the security of their home network and better understand what actions are appropriate when a certain security vulnerability is detected. Wide adoption of this tool will make consumer home IoT networks more secure.
2018-04-11
Ghanem, K., Aparicio-Navarro, F. J., Kyriakopoulos, K. G., Lambotharan, S., Chambers, J. A..  2017.  Support Vector Machine for Network Intrusion and Cyber-Attack Detection. 2017 Sensor Signal Processing for Defence Conference (SSPD). :1–5.

Cyber-security threats are a growing concern in networked environments. The development of Intrusion Detection Systems (IDSs) is fundamental in order to provide extra level of security. We have developed an unsupervised anomaly-based IDS that uses statistical techniques to conduct the detection process. Despite providing many advantages, anomaly-based IDSs tend to generate a high number of false alarms. Machine Learning (ML) techniques have gained wide interest in tasks of intrusion detection. In this work, Support Vector Machine (SVM) is deemed as an ML technique that could complement the performance of our IDS, providing a second line of detection to reduce the number of false alarms, or as an alternative detection technique. We assess the performance of our IDS against one-class and two-class SVMs, using linear and non- linear forms. The results that we present show that linear two-class SVM generates highly accurate results, and the accuracy of the linear one-class SVM is very comparable, and it does not need training datasets associated with malicious data. Similarly, the results evidence that our IDS could benefit from the use of ML techniques to increase its accuracy when analysing datasets comprising of non- homogeneous features.

Arumugam, T., Scott-Hayward, S..  2017.  Demonstrating State-Based Security Protection Mechanisms in Software Defined Networks. 2017 8th International Conference on the Network of the Future (NOF). :123–125.

The deployment of Software Defined Networking (SDN) and Network Functions Virtualization (NFV) technologies is increasing, with security as a recognized application driving adoption. However, despite the potential with SDN/NFV for automated and adaptive network security services, the controller interaction presents both a performance and scalability challenge, and a threat vector. To overcome the performance issue, stateful data-plane designs have been proposed. However, these solutions do not offer protection from SDN-specific attacks linked to necessary control functions such as link reconfiguration and switch identification. In this work, we leverage the OpenState framework to introduce state-based SDN security protection mechanisms. The extensions required for this design are presented with respect to an SDN configuration-based attack. The demonstration shows the ability of the SDN Configuration (CFG) security protection mechanism to support legitimate relocation requests and to protect against malicious connection attempts.

2018-04-02
Guan, X., Ma, Y., Hua, Y..  2017.  An Attack Intention Recognition Method Based on Evaluation Index System of Electric Power Information System. 2017 IEEE 2nd Information Technology, Networking, Electronic and Automation Control Conference (ITNEC). :1544–1548.

With the increasing scale of the network, the power information system has many characteristics, such as large number of nodes, complicated structure, diverse network protocols and abundant data, which make the network intrusion detection system difficult to detect real alarms. The current security technologies cannot meet the actual power system network security operation and protection requirements. Based on the attacker ability, the vulnerability information and the existing security protection configuration, we construct the attack sub-graphs by using the parallel distributed computing method and combine them into the whole network attack graph. The vulnerability exploit degree, attacker knowledge, attack proficiency, attacker willingness and the confidence level of the attack evidence are used to construct the security evaluation index system of the power information network system to calculate the attack probability value of each node of the attack graph. According to the probability of occurrence of each node attack, the pre-order attack path will be formed and then the most likely attack path and attack targets will be got to achieve the identification of attack intent.

Yousefi, M., Mtetwa, N., Zhang, Y., Tianfield, H..  2017.  A Novel Approach for Analysis of Attack Graph. 2017 IEEE International Conference on Intelligence and Security Informatics (ISI). :7–12.

Attack graph technique is a common tool for the evaluation of network security. However, attack graphs are generally too large and complex to be understood and interpreted by security administrators. This paper proposes an analysis framework for security attack graphs for a given IT infrastructure system. First, in order to facilitate the discovery of interconnectivities among vulnerabilities in a network, multi-host multi-stage vulnerability analysis (MulVAL) is employed to generate an attack graph for a given network topology. Then a novel algorithm is applied to refine the attack graph and generate a simplified graph called a transition graph. Next, a Markov model is used to project the future security posture of the system. Finally, the framework is evaluated by applying it on a typical IT network scenario with specific services, network configurations, and vulnerabilities.

Ádám, Norbert, Madoš, Branislav, Baláž, Anton, Pavlik, Tomáš.  2017.  Artificial Neural Network Based IDS. 2017 IEEE 15th International Symposium on Applied Machine Intelligence and Informatics (SAMI). :000159–000164.

The Network Intrusion Detection Systems (NIDS) are either signature based or anomaly based. In this paper presented NIDS system belongs to anomaly based Neural Network Intrusion Detection System (NNIDS). The proposed NNIDS is able to successfully recognize learned malicious activities in a network environment. It was tested for the SYN flood attack, UDP flood attack, nMap scanning attack, and also for non-malicious communication.

2018-03-26
d Krit, S., Haimoud, E..  2017.  Overview of Firewalls: Types and Policies: Managing Windows Embedded Firewall Programmatically. 2017 International Conference on Engineering MIS (ICEMIS). :1–7.

Due to the increasing threat of network attacks, Firewall has become crucial elements in network security, and have been widely deployed in most businesses and institutions for securing private networks. The function of a firewall is to examine each packet that passes through it and decide whether to letting them pass or halting them based on preconfigured rules and policies, so firewall now is the first defense line against cyber attacks. However most of people doesn't know how firewall works, and the most users of windows operating system doesn't know how to use the windows embedded firewall. This paper explains how firewall works, firewalls types, and all you need to know about firewall policies, then presents a novel application (QudsWall) developed by authors that manages windows embedded firewall and make it easy to use.

2018-03-05
Khalil, K., Eldash, O., Bayoumi, M..  2017.  Self-Healing Router Architecture for Reliable Network-on-Chips. 2017 24th IEEE International Conference on Electronics, Circuits and Systems (ICECS). :330–333.

NoCs are a well established research topic and several Implementations have been proposed for Self-healing. Self-healing refers to the ability of a system to detect faults or failures and fix them through healing or repairing. The main problems in current self-healing approaches are area overhead and scalability for complex structure since they are based on redundancy and spare blocks. Also, faulty router can isolate PE from other router nodes which can reduce the overall performance of the system. This paper presents a self-healing for a router to avoid denied fault PE function and isolation PE from other nodes. In the proposed design, the neighbor routers receive signal from a faulty router which keeps them to send the data packet which has only faulted router destination to a faulty router. Control unite turns on switches to connect four input ports to local ports successively to send coming packets to PE. The reliability of the proposed technique is studied and compared to conventional system with different failure rates. This approach is capable of healing 50% of the router. The area overhead is 14% for the proposed approach which is much lower compared to other approaches using redundancy.

2018-02-28
Chatfield, B., Haddad, R. J..  2017.  Moving Target Defense Intrusion Detection System for IPv6 based smart grid advanced metering infrastructure. SoutheastCon 2017. :1–7.

Conventional intrusion detection systems for smart grid communications rely heavily on static based attack detection techniques. In essence, signatures created from historical data are compared to incoming network traffic to identify abnormalities. In the case of attacks where no historical data exists, static based approaches become ineffective thus relinquishing system resilience and stability. Moving target defense (MTD) has shown to be effective in discouraging attackers by introducing system entropy to increase exploit costs. Increase in exploit cost leads to a decrease in profitability for an attacker. In this paper, a Moving Target Defense Intrusion Detection System (MTDIDS) is proposed for smart grid IPv6 based advanced metering infrastructure. The advantage of MTDIDS is the ability to detect anomalies across moving targets by means of planar keys thereupon increasing detection rate. Evaluation of MTDIDS was carried out in a smart grid advanced metering infrastructure simulated in MATLAB.

2018-02-21
Madhusudhanan, S., Mallissery, S..  2017.  Provable security analysis of complex or smart computer systems in the smart grid. 2017 IEEE International Conference on Smart Grid and Smart Cities (ICSGSC). :210–214.

Security is an important requirement of every reactive system of the smart gird. The devices connected to the smart system in smart grid are exhaustively used to provide digital information to outside world. The security of such a system is an essential requirement. The most important component of such smart systems is Operating System (OS). This paper mainly focuses on the security of OS by incorporating Access Control Mechanism (ACM) which will improve the efficiency of the smart system. The formal methods use applied mathematics for modelling and analysing of smart systems. In the proposed work Formal Security Analysis (FSA) is used with model checking and hence it helped to prove the security of smart systems. When an Operating System (OS) takes into consideration, it never comes to a halt state. In the proposed work a Transition System (TS) is designed and the desired rules of security are provided by using Linear Temporal Logics (LTL). Unlike other propositional and predicate logic, LTL can model reactive systems with a prediction for the future state of the systems. In the proposed work, Simple Promela Interpreter (SPIN) is used as a model checker that takes LTL and TS of the system as input. Hence it is possible to derive the Büchi automaton from LTL logics and that provides traces of both successful and erroneous computations. Comparison of Büchi automaton with the transition behaviour of the OS will provide the details of security violation in the system. Validation of automaton operations on infinite computational sequences verify that whether systems are provably secure or not. Hence the proposed formal security analysis will provably ensures the security of smart systems in the area of smart grid applications.