Pertanyaan berikut telah muncul beberapa kali saat menguji keamanan sistem atau model.
Motivasi: Kelemahan keamanan perangkat lunak sering kali bukan berasal dari bug karena input yang valid, tetapi bug yang dihasilkan dari input tidak valid yang cukup dekat dengan input yang valid untuk melewati banyak pemeriksaan validitas langsung. Contoh klasiknya tentu saja buffer overflows, di mana inputnya masuk akal, kecuali bahwa itu terlalu besar. Kompiler dan alat lain dapat membantu mengatasi masalah ini dengan memodifikasi tata letak tumpukan dan tumpukan dan dengan teknik kebingungan lainnya. Alternatifnya adalah menghapus masalah dari kode sumber itu sendiri. Salah satu teknik yang disebut fuzzing bombardir program dengan input mendekati input yang diharapkan, tetapi di beberapa tempat tidak masuk akal (nilai besar untuk bidang bilangan bulat atau string). Saya ingin memahami fuzzing (sebagai salah satu contoh) dari perspektif yang lebih formal.
Asumsikan bahwa ruang input yang valid dijelaskan oleh kendala . Biarkan M menjadi himpunan solusi dari kendala tersebut, yaitu M = { m ∈ M | m ⊨ Φ } , di mana M adalah ruang input yang memungkinkan.
Saya mencari pekerjaan yang menggambarkan gagasan berikut:
The penumbra dari adalah seperangkat M ' ⊆ M sehingga untuk setiap m ∈ M ' m ⊭ Φ dan dalam beberapa pengertian unsur M ' yang dekat dengan unsur-unsur M . Orang dapat menganggap penumbra sebagai solusi yang hampir . Tentu saja, gagasan ini tidak akan unik.
Cara mengendurkan kendala hingga Φ ′ sedemikian rupa sehingga pertama-tama Φ ⇒ Φ ′ dan Φ ′ ∧ ¬ Φ adalah, dalam arti tertentu, penumbra sintaksis dari Φ .
"Penumbra" adalah kata yang saya pilih untuk menggambarkan konsep. Mungkin juga disebut sesuatu yang lain.
Saya menemukan inspirasi dalam morfologi matematika , karenanya metafora visual saya, tetapi dua dunia terpisah parsec. Apakah ada pekerjaan yang bermanfaat di sana? Atau mungkin di dunia set kasar ?
Adakah yang bisa menjelaskan?
Jawaban:
Sebagian besar perhatian diberikan pada varian optimisasi dari masalah kepuasan kendala (CSP) yang difokuskan pada pemenuhan sejumlah kendala (MAX-CSP), atau dalam kasus Boolean dalam memilih solusi yang memberikan variabel sebanyak mungkin variabel nilai 1 ( MAX-ONES, ada juga MIN-ONES).
Sebagai gantinya, Anda bertanya tentang varian yang bisa disebut CSP PARTIMAL MAKSIMUM. Ini dipelajari setidaknya sampai akhir 1960-an, tetapi saya tidak menyadarinya memiliki nama mapan. Ini adalah masalah alami, dan akan baik untuk melihat lebih banyak pekerjaan yang menyelidikinya. Terima kasih telah menyediakan aplikasi potensial lain untuk masalah ini!
Satu set penugasan variabel-nilai disebut penugasan parsial . Satu dapat menulis tugas nilai variabel sebagai tuple (variabel, nilai). Tugas parsial kemudian hanya berfungsi dari variabel ke nilai. Alat peraga adalah tugas sebagian yang tidak melanggar batasan apa pun. Sama, prop tidak berisi tugas parsial yang dilarang oleh beberapa kendala (sebagai subset).
Salah satu cara untuk mengungkapkan masalah optimisasi adalah sebagai berikut.
Bagian kedua dari pertanyaan Anda juga tampak sangat menarik, tetapi saya tidak mengetahui adanya pekerjaan yang terkait dengannya.
Catatan Kaki: Istilah prop berasal dari tesis saya; itu dimaksudkan untuk menyampaikan gagasan bahwa penugasan sebagian seperti itu tepat, dan juga bahwa mereka mendukung serangkaian solusi. Ini berbeda dengan nogood , yang merupakan istilah yang diterima untuk menggambarkan penugasan sebagian yang tidak dapat diperluas ke solusi. Kata "nogood" diperkenalkan oleh Richard Stallman dan Gerald Sussman pada tahun 1976, ketika RMS masih merupakan peneliti AI dan bukan aktivis kebebasan perangkat lunak.
sumber