KasperskyOS Community Edition 1.2

/* Test set that includes only one test. */ assert "some tests" { /* Test that includes four test cases. */ sequence "first sequence" { /* It is expected that startup of a Server-class process is allowed. * If this is true, the s variable will be assigned the SID value * of the started Server-class process. */ s <- execute dst=Server /* It is expected that startup of a Client-class process is allowed. * If this is true, the c variable will be assigned the SID value * of the started Client-class process. */ c <- execute dst=Client /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ grant "Client calls Ping" request src=c dst=s endpoint=pingComp.pingImpl method=Ping { value : 100 } /* It is expected that a server of the Server class is not allowed to respond to a client * of the Client class if the client calls the Ping method of the pingComp.pingImpl endpoint. * (The IPC response does not contain any parameters because the Ping interface method * has no output parameters.) */ deny "Server cannot respond" response src=s dst=c endpoint=pingComp.pingImpl method=Ping {} } }

/* Test set that includes two tests. */ assert "ping tests"{ /* Initial part of each of the two tests that includes two test cases. */ setup { /* It is expected that startup of a Server-class process is allowed. * If this is true, the s variable will be assigned the SID value * of the started Server-class process. */ s <- execute dst=Server /* It is expected that startup of a Client-class process is allowed. * If this is true, the c variable will be assigned the SID value * of the started Client-class process. */ c <- execute dst=Client } /* Test that includes four test cases: two test cases * in the initial part and two test cases in the main part.*/ sequence "ping-ping is denied" { /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ c ~> s : pingComp.pingImpl.Ping { value : 100 } /* It is expected that a client of the Client class is not allowed to query * a server of the Server class by once again calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ deny c ~> s : pingComp.pingImpl.Ping { value : 100 } } /* Test that includes four test cases: two test cases * in the initial part and two test cases in the main part. */ sequence "ping-pong is granted" { /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ c ~> s : pingComp.pingImpl.Ping { value: 100 } /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Pong method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ c ~> s : pingComp.pingImpl.Pong { value: 100 } } }

/* Test set that includes only one test. */ assert { /* Test that includes eight test cases. */ sequence { storage <− execute dst=test.kl.UpdateStorage manager <− execute dst=test.kl.UpdateManager deployer <− execute dst=test.kl.UpdateDeployer downloader <− execute dst=test.kl.UpdateDownloader grant manager ~> downloader:UpdateDownloader.Downloader.LoadPackage { url : ”url012345678” } grant response src=downloader dst=manager endpoint=UpdateDownloader.Downloader method=LoadPackage { handle : 29, result : 1 } deny manager ~> deployer:UpdateDeployer.Deployer.Start { handle : 29 } deny request src=manager dst=deployer endpoint=UpdateDeployer.Deployer method=Start { handle : 29 } } }